ceqsex3v

Description: Elimination of three existential quantifiers, using implicit substitution. (Contributed by NM, 16-Aug-2011)

	Ref	Expression
Hypotheses	ceqsex3v.1	⊢ 𝐴 ∈ V
	ceqsex3v.2	⊢ 𝐵 ∈ V
	ceqsex3v.3	⊢ 𝐶 ∈ V
	ceqsex3v.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	ceqsex3v.5	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	ceqsex3v.6	⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
Assertion	ceqsex3v	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ↔ 𝜃 )

Proof

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

Metamath Proof Explorer

Theorem ceqsex3v

Proof