Metamath Proof Explorer

Theorem ov2gf

Description: The value of an operation class abstraction. A version of ovmpog using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006) (Revised by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypotheses ov2gf.a 
|- F/_ x A
ov2gf.c 
|- F/_ y A
ov2gf.d 
|- F/_ y B
ov2gf.1 
|- F/_ x G
ov2gf.2 
|- F/_ y S
ov2gf.3 
|- ( x = A -> R = G )
ov2gf.4 
|- ( y = B -> G = S )
ov2gf.5 
|- F = ( x e. C , y e. D |-> R )
Assertion ov2gf 
|- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )

Proof

Step Hyp Ref Expression
1 ov2gf.a 
 |-  F/_ x A
2 ov2gf.c 
 |-  F/_ y A
3 ov2gf.d 
 |-  F/_ y B
4 ov2gf.1 
 |-  F/_ x G
5 ov2gf.2 
 |-  F/_ y S
6 ov2gf.3 
 |-  ( x = A -> R = G )
7 ov2gf.4 
 |-  ( y = B -> G = S )
8 ov2gf.5 
 |-  F = ( x e. C , y e. D |-> R )
9 elex 
 |-  ( S e. H -> S e. _V )
10 4 nfel1 
 |-  F/ x G e. _V
11 nfmpo1 
 |-  F/_ x ( x e. C , y e. D |-> R )
12 8 11 nfcxfr 
 |-  F/_ x F
13 nfcv 
 |-  F/_ x y
14 1 12 13 nfov 
 |-  F/_ x ( A F y )
15 14 4 nfeq 
 |-  F/ x ( A F y ) = G
16 10 15 nfim 
 |-  F/ x ( G e. _V -> ( A F y ) = G )
17 5 nfel1 
 |-  F/ y S e. _V
18 nfmpo2 
 |-  F/_ y ( x e. C , y e. D |-> R )
19 8 18 nfcxfr 
 |-  F/_ y F
20 2 19 3 nfov 
 |-  F/_ y ( A F B )
21 20 5 nfeq 
 |-  F/ y ( A F B ) = S
22 17 21 nfim 
 |-  F/ y ( S e. _V -> ( A F B ) = S )
23 6 eleq1d 
 |-  ( x = A -> ( R e. _V <-> G e. _V ) )
24 oveq1 
 |-  ( x = A -> ( x F y ) = ( A F y ) )
25 24 6 eqeq12d 
 |-  ( x = A -> ( ( x F y ) = R <-> ( A F y ) = G ) )
26 23 25 imbi12d 
 |-  ( x = A -> ( ( R e. _V -> ( x F y ) = R ) <-> ( G e. _V -> ( A F y ) = G ) ) )
27 7 eleq1d 
 |-  ( y = B -> ( G e. _V <-> S e. _V ) )
28 oveq2 
 |-  ( y = B -> ( A F y ) = ( A F B ) )
29 28 7 eqeq12d 
 |-  ( y = B -> ( ( A F y ) = G <-> ( A F B ) = S ) )
30 27 29 imbi12d 
 |-  ( y = B -> ( ( G e. _V -> ( A F y ) = G ) <-> ( S e. _V -> ( A F B ) = S ) ) )
31 8 ovmpt4g 
 |-  ( ( x e. C /\ y e. D /\ R e. _V ) -> ( x F y ) = R )
32 31 3expia 
 |-  ( ( x e. C /\ y e. D ) -> ( R e. _V -> ( x F y ) = R ) )
33 1 2 3 16 22 26 30 32 vtocl2gaf 
 |-  ( ( A e. C /\ B e. D ) -> ( S e. _V -> ( A F B ) = S ) )
34 9 33 syl5 
 |-  ( ( A e. C /\ B e. D ) -> ( S e. H -> ( A F B ) = S ) )
35 34 3impia 
 |-  ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )