Metamath Proof Explorer

Theorem ceqsex2

Description: Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006)

Ref Expression
Hypotheses ceqsex2.1 ⊢Ⅎxψ
ceqsex2.2 ⊢Ⅎyχ
ceqsex2.3 ⊢A∈V
ceqsex2.4 ⊢B∈V
ceqsex2.5 ⊢x=A→φ↔ψ
ceqsex2.6 ⊢y=B→ψ↔χ
Assertion ceqsex2 ⊢∃x∃yx=A∧y=B∧φ↔χ

Proof

Step Hyp Ref Expression
1 ceqsex2.1 ⊢Ⅎxψ
2 ceqsex2.2 ⊢Ⅎyχ
3 ceqsex2.3 ⊢A∈V
4 ceqsex2.4 ⊢B∈V
5 ceqsex2.5 ⊢x=A→φ↔ψ
6 ceqsex2.6 ⊢y=B→ψ↔χ
7 3anass ⊢x=A∧y=B∧φ↔x=A∧y=B∧φ
8 7 exbii ⊢∃yx=A∧y=B∧φ↔∃yx=A∧y=B∧φ
9 19.42v ⊢∃yx=A∧y=B∧φ↔x=A∧∃yy=B∧φ
10 8 9 bitri ⊢∃yx=A∧y=B∧φ↔x=A∧∃yy=B∧φ
11 10 exbii ⊢∃x∃yx=A∧y=B∧φ↔∃xx=A∧∃yy=B∧φ
12 nfv ⊢Ⅎxy=B
13 12 1 nfan ⊢Ⅎxy=B∧ψ
14 13 nfex ⊢Ⅎx∃yy=B∧ψ
15 5 anbi2d ⊢x=A→y=B∧φ↔y=B∧ψ
16 15 exbidv ⊢x=A→∃yy=B∧φ↔∃yy=B∧ψ
17 14 3 16 ceqsex ⊢∃xx=A∧∃yy=B∧φ↔∃yy=B∧ψ
18 2 4 6 ceqsex ⊢∃yy=B∧ψ↔χ
19 11 17 18 3bitri ⊢∃x∃yx=A∧y=B∧φ↔χ