Metamath Proof Explorer

Theorem copsex2gOLD

Description: Obsolete version of copsex2g as of 1-Sep-2024. (Contributed by NM, 28-May-1995) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis copsex2g.1 ⊢ x = A ∧ y = B → φ ↔ ψ
Assertion copsex2gOLD ⊢ A ∈ V ∧ B ∈ W → ∃ x ∃ y A B = x y ∧ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 copsex2g.1 ⊢ x = A ∧ y = B → φ ↔ ψ
2 elisset ⊢ A ∈ V → ∃ x x = A
3 elisset ⊢ B ∈ W → ∃ y y = B
4 exdistrv ⊢ ∃ x ∃ y x = A ∧ y = B ↔ ∃ x x = A ∧ ∃ y y = B
5 nfe1 ⊢ Ⅎ x ∃ x ∃ y A B = x y ∧ φ
6 nfv ⊢ Ⅎ x ψ
7 5 6 nfbi ⊢ Ⅎ x ∃ x ∃ y A B = x y ∧ φ ↔ ψ
8 nfe1 ⊢ Ⅎ y ∃ y A B = x y ∧ φ
9 8 nfex ⊢ Ⅎ y ∃ x ∃ y A B = x y ∧ φ
10 nfv ⊢ Ⅎ y ψ
11 9 10 nfbi ⊢ Ⅎ y ∃ x ∃ y A B = x y ∧ φ ↔ ψ
12 opeq12 ⊢ x = A ∧ y = B → x y = A B
13 copsexgw ⊢ A B = x y → φ ↔ ∃ x ∃ y A B = x y ∧ φ
14 13 eqcoms ⊢ x y = A B → φ ↔ ∃ x ∃ y A B = x y ∧ φ
15 12 14 syl ⊢ x = A ∧ y = B → φ ↔ ∃ x ∃ y A B = x y ∧ φ
16 15 1 bitr3d ⊢ x = A ∧ y = B → ∃ x ∃ y A B = x y ∧ φ ↔ ψ
17 11 16 exlimi ⊢ ∃ y x = A ∧ y = B → ∃ x ∃ y A B = x y ∧ φ ↔ ψ
18 7 17 exlimi ⊢ ∃ x ∃ y x = A ∧ y = B → ∃ x ∃ y A B = x y ∧ φ ↔ ψ
19 4 18 sylbir ⊢ ∃ x x = A ∧ ∃ y y = B → ∃ x ∃ y A B = x y ∧ φ ↔ ψ
20 2 3 19 syl2an ⊢ A ∈ V ∧ B ∈ W → ∃ x ∃ y A B = x y ∧ φ ↔ ψ