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 ⊢ 𝐴 ∈ V
ceqsex2v.2 ⊢ 𝐵 ∈ V
ceqsex2v.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
ceqsex2v.4 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
Assertion ceqsex2v ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ 𝜒 )

Proof

Step Hyp Ref Expression
1 ceqsex2v.1 ⊢ 𝐴 ∈ V
2 ceqsex2v.2 ⊢ 𝐵 ∈ V
3 ceqsex2v.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4 ceqsex2v.4 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
5 3anass ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
6 5 exbii ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
7 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
8 6 7 bitri ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
9 8 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
10 3 anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ( 𝑦 = 𝐵 ∧ 𝜓 ) ) )
11 10 exbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜓 ) ) )
12 1 11 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜓 ) )
13 2 4 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜓 ) ↔ 𝜒 )
14 9 12 13 3bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ 𝜒 )