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

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 ∃ y x = 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 ⊢ ∃ y x = A ∧ y = B ∧ φ ↔ ∃ y x = A ∧ y = B ∧ φ
9 19.42v ⊢ ∃ y x = A ∧ y = B ∧ φ ↔ x = A ∧ ∃ y y = B ∧ φ
10 8 9 bitri ⊢ ∃ y x = A ∧ y = B ∧ φ ↔ x = A ∧ ∃ y y = B ∧ φ
11 10 exbii ⊢ ∃ x ∃ y x = A ∧ y = B ∧ φ ↔ ∃ x x = A ∧ ∃ y y = B ∧ φ
12 nfv ⊢ Ⅎ x y = B
13 12 1 nfan ⊢ Ⅎ x y = B ∧ ψ
14 13 nfex ⊢ Ⅎ x ∃ y y = B ∧ ψ
15 5 anbi2d ⊢ x = A → y = B ∧ φ ↔ y = B ∧ ψ
16 15 exbidv ⊢ x = A → ∃ y y = B ∧ φ ↔ ∃ y y = B ∧ ψ
17 14 3 16 ceqsex ⊢ ∃ x x = A ∧ ∃ y y = B ∧ φ ↔ ∃ y y = B ∧ ψ
18 2 4 6 ceqsex ⊢ ∃ y y = B ∧ ψ ↔ χ
19 11 17 18 3bitri ⊢ ∃ x ∃ y x = A ∧ y = B ∧ φ ↔ χ