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

Metamath Proof Explorer

Theorem ovmpoga

Description: Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypotheses ovmpoga.1 
|- ( ( x = A /\ y = B ) -> R = S )
ovmpoga.2 
|- F = ( x e. C , y e. D |-> R )
Assertion ovmpoga 
|- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )

Proof

Step Hyp Ref Expression
1 ovmpoga.1 
 |-  ( ( x = A /\ y = B ) -> R = S )
2 ovmpoga.2 
 |-  F = ( x e. C , y e. D |-> R )
3 elex 
 |-  ( S e. H -> S e. _V )
4 2 a1i 
 |-  ( ( A e. C /\ B e. D /\ S e. _V ) -> F = ( x e. C , y e. D |-> R ) )
5 1 adantl 
 |-  ( ( ( A e. C /\ B e. D /\ S e. _V ) /\ ( x = A /\ y = B ) ) -> R = S )
6 simp1 
 |-  ( ( A e. C /\ B e. D /\ S e. _V ) -> A e. C )
7 simp2 
 |-  ( ( A e. C /\ B e. D /\ S e. _V ) -> B e. D )
8 simp3 
 |-  ( ( A e. C /\ B e. D /\ S e. _V ) -> S e. _V )
9 4 5 6 7 8 ovmpod 
 |-  ( ( A e. C /\ B e. D /\ S e. _V ) -> ( A F B ) = S )
10 3 9 syl3an3 
 |-  ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )