Theorem rspceov

Description: A frequently used special case of rspc2ev for operation values. (Contributed by NM, 21-Mar-2007)

	Ref	Expression
Assertion	rspceov	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = ( 𝐶 𝐹 𝐷 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑆 = ( 𝑥 𝐹 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = 𝐶 → ( 𝑥 𝐹 𝑦 ) = ( 𝐶 𝐹 𝑦 ) )
2	1	eqeq2d	⊢ ( 𝑥 = 𝐶 → ( 𝑆 = ( 𝑥 𝐹 𝑦 ) ↔ 𝑆 = ( 𝐶 𝐹 𝑦 ) ) )
3		oveq2	⊢ ( 𝑦 = 𝐷 → ( 𝐶 𝐹 𝑦 ) = ( 𝐶 𝐹 𝐷 ) )
4	3	eqeq2d	⊢ ( 𝑦 = 𝐷 → ( 𝑆 = ( 𝐶 𝐹 𝑦 ) ↔ 𝑆 = ( 𝐶 𝐹 𝐷 ) ) )
5	2 4	rspc2ev	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = ( 𝐶 𝐹 𝐷 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑆 = ( 𝑥 𝐹 𝑦 ) )