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

Metamath Proof Explorer

Theorem ceqsex2v

Description: Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006) Avoid ax-10 and ax-11 . (Revised by GG, 20-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 ceqsex2v.1 ⊢ A ∈ V
2 ceqsex2v.2 ⊢ B ∈ V
3 ceqsex2v.3 ⊢ x = A → φ ↔ ψ
4 ceqsex2v.4 ⊢ y = B → ψ ↔ χ
5 3anass ⊢ x = A ∧ y = B ∧ φ ↔ x = A ∧ y = B ∧ φ
6 5 exbii ⊢ ∃ y x = A ∧ y = B ∧ φ ↔ ∃ y x = A ∧ y = B ∧ φ
7 19.42v ⊢ ∃ y x = A ∧ y = B ∧ φ ↔ x = A ∧ ∃ y y = B ∧ φ
8 6 7 bitri ⊢ ∃ y x = A ∧ y = B ∧ φ ↔ x = A ∧ ∃ y y = B ∧ φ
9 8 exbii ⊢ ∃ x ∃ y x = A ∧ y = B ∧ φ ↔ ∃ x x = A ∧ ∃ y y = B ∧ φ
10 3 anbi2d ⊢ x = A → y = B ∧ φ ↔ y = B ∧ ψ
11 10 exbidv ⊢ x = A → ∃ y y = B ∧ φ ↔ ∃ y y = B ∧ ψ
12 1 11 ceqsexv ⊢ ∃ x x = A ∧ ∃ y y = B ∧ φ ↔ ∃ y y = B ∧ ψ
13 2 4 ceqsexv ⊢ ∃ y y = B ∧ ψ ↔ χ
14 9 12 13 3bitri ⊢ ∃ x ∃ y x = A ∧ y = B ∧ φ ↔ χ