Theorem rspceaov

Description: A frequently used special case of rspc2ev for operation values, analogous to rspceov . (Contributed by Alexander van der Vekens, 26-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( 𝑥 = 𝐶 → 𝐹 = 𝐹 )
2		id	⊢ ( 𝑥 = 𝐶 → 𝑥 = 𝐶 )
3		eqidd	⊢ ( 𝑥 = 𝐶 → 𝑦 = 𝑦 )
4	1 2 3	aoveq123d	⊢ ( 𝑥 = 𝐶 → (( 𝑥 𝐹 𝑦 )) = (( 𝐶 𝐹 𝑦 )) )
5	4	eqeq2d	⊢ ( 𝑥 = 𝐶 → ( 𝑆 = (( 𝑥 𝐹 𝑦 )) ↔ 𝑆 = (( 𝐶 𝐹 𝑦 )) ) )
6		eqidd	⊢ ( 𝑦 = 𝐷 → 𝐹 = 𝐹 )
7		eqidd	⊢ ( 𝑦 = 𝐷 → 𝐶 = 𝐶 )
8		id	⊢ ( 𝑦 = 𝐷 → 𝑦 = 𝐷 )
9	6 7 8	aoveq123d	⊢ ( 𝑦 = 𝐷 → (( 𝐶 𝐹 𝑦 )) = (( 𝐶 𝐹 𝐷 )) )
10	9	eqeq2d	⊢ ( 𝑦 = 𝐷 → ( 𝑆 = (( 𝐶 𝐹 𝑦 )) ↔ 𝑆 = (( 𝐶 𝐹 𝐷 )) ) )
11	5 10	rspc2ev	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (( 𝐶 𝐹 𝐷 )) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑆 = (( 𝑥 𝐹 𝑦 )) )