Theorem rspc2ev

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999)

	Ref	Expression
Hypotheses	rspc2v.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
	rspc2v.2	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
Assertion	rspc2ev	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rspc2v.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
2		rspc2v.2	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
3	2	rspcev	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝜓 ) → ∃ 𝑦 ∈ 𝐷 𝜒 )
4	3	anim2i	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ( 𝐵 ∈ 𝐷 ∧ 𝜓 ) ) → ( 𝐴 ∈ 𝐶 ∧ ∃ 𝑦 ∈ 𝐷 𝜒 ) )
5	4	3impb	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓 ) → ( 𝐴 ∈ 𝐶 ∧ ∃ 𝑦 ∈ 𝐷 𝜒 ) )
6	1	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∈ 𝐷 𝜑 ↔ ∃ 𝑦 ∈ 𝐷 𝜒 ) )
7	6	rspcev	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ∃ 𝑦 ∈ 𝐷 𝜒 ) → ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 𝜑 )
8	5 7	syl	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 𝜑 )