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	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑 ) ↔ 𝜒 )