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	1	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∈ 𝐷 𝜑 ↔ ∃ 𝑦 ∈ 𝐷 𝜒 ) )
4		simp1	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓 ) → 𝐴 ∈ 𝐶 )
5	2	rspcev	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝜓 ) → ∃ 𝑦 ∈ 𝐷 𝜒 )
6	5	3adant1	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓 ) → ∃ 𝑦 ∈ 𝐷 𝜒 )
7	3 4 6	rspcedvdw	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 𝜑 )