Metamath Proof Explorer

Theorem cgsex2gd

Description: Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995) Adapt cgsex2g to deduction form. (Revised by BJ, 28-Mar-2026) Do not use cgsex2g . (Proof modification is discouraged.)

Ref Expression
Hypotheses cgsex2gd.is ⊢ φ ∧ x = A ∧ y = B → ψ
cgsex2gd.maj ⊢ φ ∧ ψ → χ ↔ θ
Assertion cgsex2gd ⊢ φ ∧ A ∈ V ∧ B ∈ W → ∃ x ∃ y ψ ∧ χ ↔ θ

Proof

Step Hyp Ref Expression
1 cgsex2gd.is ⊢ φ ∧ x = A ∧ y = B → ψ
2 cgsex2gd.maj ⊢ φ ∧ ψ → χ ↔ θ
3 2 biimp3a ⊢ φ ∧ ψ ∧ χ → θ
4 3 3expib ⊢ φ → ψ ∧ χ → θ
5 4 exlimdvv ⊢ φ → ∃ x ∃ y ψ ∧ χ → θ
6 5 adantr ⊢ φ ∧ A ∈ V ∧ B ∈ W → ∃ x ∃ y ψ ∧ χ → θ
7 1 ex ⊢ φ → x = A ∧ y = B → ψ
8 7 2eximdv ⊢ φ → ∃ x ∃ y x = A ∧ y = B → ∃ x ∃ y ψ
9 elisset ⊢ A ∈ V → ∃ x x = A
10 elisset ⊢ B ∈ W → ∃ y y = B
11 9 10 anim12i ⊢ A ∈ V ∧ B ∈ W → ∃ x x = A ∧ ∃ y y = B
12 exdistrv ⊢ ∃ x ∃ y x = A ∧ y = B ↔ ∃ x x = A ∧ ∃ y y = B
13 11 12 sylibr ⊢ A ∈ V ∧ B ∈ W → ∃ x ∃ y x = A ∧ y = B
14 8 13 impel ⊢ φ ∧ A ∈ V ∧ B ∈ W → ∃ x ∃ y ψ
15 2 biimprd ⊢ φ ∧ ψ → θ → χ
16 15 impancom ⊢ φ ∧ θ → ψ → χ
17 16 ancld ⊢ φ ∧ θ → ψ → ψ ∧ χ
18 17 2eximdv ⊢ φ ∧ θ → ∃ x ∃ y ψ → ∃ x ∃ y ψ ∧ χ
19 18 expimpd ⊢ φ → θ ∧ ∃ x ∃ y ψ → ∃ x ∃ y ψ ∧ χ
20 19 adantr ⊢ φ ∧ A ∈ V ∧ B ∈ W → θ ∧ ∃ x ∃ y ψ → ∃ x ∃ y ψ ∧ χ
21 14 20 mpan2d ⊢ φ ∧ A ∈ V ∧ B ∈ W → θ → ∃ x ∃ y ψ ∧ χ
22 6 21 impbid ⊢ φ ∧ A ∈ V ∧ B ∈ W → ∃ x ∃ y ψ ∧ χ ↔ θ