This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem or2expropbilem2

Description: Lemma 2 for or2expropbi and ich2exprop . (Contributed by AV, 16-Jul-2023)

Ref Expression
Assertion or2expropbilem2 ⊢ ∃ a ∃ b A B = a b ∧ φ ↔ ∃ x ∃ y A B = x y ∧ [˙y / b]˙ [˙x / a]˙ φ

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ x A B = a b ∧ φ
2 nfv ⊢ Ⅎ y A B = a b ∧ φ
3 nfv ⊢ Ⅎ a A B = x y
4 nfcv ⊢ Ⅎ _ a y
5 nfsbc1v ⊢ Ⅎ a [˙x / a]˙ φ
6 4 5 nfsbcw ⊢ Ⅎ a [˙y / b]˙ [˙x / a]˙ φ
7 3 6 nfan ⊢ Ⅎ a A B = x y ∧ [˙y / b]˙ [˙x / a]˙ φ
8 nfv ⊢ Ⅎ b A B = x y
9 nfsbc1v ⊢ Ⅎ b [˙y / b]˙ [˙x / a]˙ φ
10 8 9 nfan ⊢ Ⅎ b A B = x y ∧ [˙y / b]˙ [˙x / a]˙ φ
11 opeq12 ⊢ a = x ∧ b = y → a b = x y
12 11 eqeq2d ⊢ a = x ∧ b = y → A B = a b ↔ A B = x y
13 sbceq1a ⊢ a = x → φ ↔ [˙x / a]˙ φ
14 sbceq1a ⊢ b = y → [˙x / a]˙ φ ↔ [˙y / b]˙ [˙x / a]˙ φ
15 13 14 sylan9bb ⊢ a = x ∧ b = y → φ ↔ [˙y / b]˙ [˙x / a]˙ φ
16 12 15 anbi12d ⊢ a = x ∧ b = y → A B = a b ∧ φ ↔ A B = x y ∧ [˙y / b]˙ [˙x / a]˙ φ
17 1 2 7 10 16 cbvex2v ⊢ ∃ a ∃ b A B = a b ∧ φ ↔ ∃ x ∃ y A B = x y ∧ [˙y / b]˙ [˙x / a]˙ φ