This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspceov

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

Ref Expression
Assertion rspceov ⊢ C ∈ A ∧ D ∈ B ∧ S = C F D → ∃ x ∈ A ∃ y ∈ B S = x F y

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ x = C → x F y = C F y
2 1 eqeq2d ⊢ x = C → S = x F y ↔ S = C F y
3 oveq2 ⊢ y = D → C F y = C F D
4 3 eqeq2d ⊢ y = D → S = C F y ↔ S = C F D
5 2 4 rspc2ev ⊢ C ∈ A ∧ D ∈ B ∧ S = C F D → ∃ x ∈ A ∃ y ∈ B S = x F y