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 ) |