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