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

Proof

Step Hyp Ref Expression
1 ceqsex2.1 ⊢ Ⅎ 𝑥 𝜓
2 ceqsex2.2 ⊢ Ⅎ 𝑦 𝜒
3 ceqsex2.3 ⊢ 𝐴 ∈ V
4 ceqsex2.4 ⊢ 𝐵 ∈ V
5 ceqsex2.5 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
6 ceqsex2.6 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
7 3anass ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
8 7 exbii ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
9 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
10 8 9 bitri ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
11 10 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
12 nfv ⊢ Ⅎ 𝑥 𝑦 = 𝐵
13 12 1 nfan ⊢ Ⅎ 𝑥 ( 𝑦 = 𝐵 ∧ 𝜓 )
14 13 nfex ⊢ Ⅎ 𝑥 ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜓 )
15 5 anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ( 𝑦 = 𝐵 ∧ 𝜓 ) ) )
16 15 exbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜓 ) ) )
17 14 3 16 ceqsex ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜓 ) )
18 2 4 6 ceqsex ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜓 ) ↔ 𝜒 )
19 11 17 18 3bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ 𝜒 )