Metamath Proof Explorer

Theorem cgsex2g

Description: Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995)

Ref Expression
Hypotheses cgsex2g.1 ⊢ x = A ∧ y = B → χ
cgsex2g.2 ⊢ χ → φ ↔ ψ
Assertion cgsex2g ⊢ A ∈ V ∧ B ∈ W → ∃ x ∃ y χ ∧ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 cgsex2g.1 ⊢ x = A ∧ y = B → χ
2 cgsex2g.2 ⊢ χ → φ ↔ ψ
3 2 biimpa ⊢ χ ∧ φ → ψ
4 3 exlimivv ⊢ ∃ x ∃ y χ ∧ φ → ψ
5 elisset ⊢ A ∈ V → ∃ x x = A
6 elisset ⊢ B ∈ W → ∃ y y = B
7 5 6 anim12i ⊢ A ∈ V ∧ B ∈ W → ∃ x x = A ∧ ∃ y y = B
8 exdistrv ⊢ ∃ x ∃ y x = A ∧ y = B ↔ ∃ x x = A ∧ ∃ y y = B
9 7 8 sylibr ⊢ A ∈ V ∧ B ∈ W → ∃ x ∃ y x = A ∧ y = B
10 1 2eximi ⊢ ∃ x ∃ y x = A ∧ y = B → ∃ x ∃ y χ
11 9 10 syl ⊢ A ∈ V ∧ B ∈ W → ∃ x ∃ y χ
12 2 biimprcd ⊢ ψ → χ → φ
13 12 ancld ⊢ ψ → χ → χ ∧ φ
14 13 2eximdv ⊢ ψ → ∃ x ∃ y χ → ∃ x ∃ y χ ∧ φ
15 11 14 syl5com ⊢ A ∈ V ∧ B ∈ W → ψ → ∃ x ∃ y χ ∧ φ
16 4 15 impbid2 ⊢ A ∈ V ∧ B ∈ W → ∃ x ∃ y χ ∧ φ ↔ ψ