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

Metamath Proof Explorer

Theorem ceqsex4v

Description: Elimination of four existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011)

Ref Expression
Hypotheses ceqsex4v.1 ⊢ 𝐴 ∈ V
ceqsex4v.2 ⊢ 𝐵 ∈ V
ceqsex4v.3 ⊢ 𝐶 ∈ V
ceqsex4v.4 ⊢ 𝐷 ∈ V
ceqsex4v.7 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
ceqsex4v.8 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
ceqsex4v.9 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
ceqsex4v.10 ⊢ ( 𝑤 = 𝐷 → ( 𝜃 ↔ 𝜏 ) )
Assertion ceqsex4v ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) ↔ 𝜏 )

Proof

Step Hyp Ref Expression
1 ceqsex4v.1 ⊢ 𝐴 ∈ V
2 ceqsex4v.2 ⊢ 𝐵 ∈ V
3 ceqsex4v.3 ⊢ 𝐶 ∈ V
4 ceqsex4v.4 ⊢ 𝐷 ∈ V
5 ceqsex4v.7 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
6 ceqsex4v.8 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
7 ceqsex4v.9 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
8 ceqsex4v.10 ⊢ ( 𝑤 = 𝐷 → ( 𝜃 ↔ 𝜏 ) )
9 19.42vv ⊢ ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) )
10 3anass ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) ) )
11 df-3an ⊢ ( ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ↔ ( ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) )
12 11 anbi2i ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) ) )
13 10 12 bitr4i ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) )
14 13 2exbii ⊢ ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) )
15 df-3an ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) )
16 9 14 15 3bitr4i ⊢ ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) )
17 16 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) )
18 5 3anbi3d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ↔ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜓 ) ) )
19 18 2exbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜓 ) ) )
20 6 3anbi3d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜓 ) ↔ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜒 ) ) )
21 20 2exbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜓 ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜒 ) ) )
22 1 2 19 21 ceqsex2v ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜑 ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜒 ) )
23 3 4 7 8 ceqsex2v ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ∧ 𝜒 ) ↔ 𝜏 )
24 17 22 23 3bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ 𝜑 ) ↔ 𝜏 )