Step |
Hyp |
Ref |
Expression |
1 |
|
ovmpos.3 |
|- F = ( x e. C , y e. D |-> R ) |
2 |
|
elex |
|- ( [_ A / x ]_ [_ B / y ]_ R e. V -> [_ A / x ]_ [_ B / y ]_ R e. _V ) |
3 |
|
nfcv |
|- F/_ x A |
4 |
|
nfcv |
|- F/_ y A |
5 |
|
nfcv |
|- F/_ y B |
6 |
|
nfcsb1v |
|- F/_ x [_ A / x ]_ R |
7 |
6
|
nfel1 |
|- F/ x [_ A / x ]_ R e. _V |
8 |
|
nfmpo1 |
|- F/_ x ( x e. C , y e. D |-> R ) |
9 |
1 8
|
nfcxfr |
|- F/_ x F |
10 |
|
nfcv |
|- F/_ x y |
11 |
3 9 10
|
nfov |
|- F/_ x ( A F y ) |
12 |
11 6
|
nfeq |
|- F/ x ( A F y ) = [_ A / x ]_ R |
13 |
7 12
|
nfim |
|- F/ x ( [_ A / x ]_ R e. _V -> ( A F y ) = [_ A / x ]_ R ) |
14 |
|
nfcsb1v |
|- F/_ y [_ B / y ]_ [_ A / x ]_ R |
15 |
14
|
nfel1 |
|- F/ y [_ B / y ]_ [_ A / x ]_ R e. _V |
16 |
|
nfmpo2 |
|- F/_ y ( x e. C , y e. D |-> R ) |
17 |
1 16
|
nfcxfr |
|- F/_ y F |
18 |
4 17 5
|
nfov |
|- F/_ y ( A F B ) |
19 |
18 14
|
nfeq |
|- F/ y ( A F B ) = [_ B / y ]_ [_ A / x ]_ R |
20 |
15 19
|
nfim |
|- F/ y ( [_ B / y ]_ [_ A / x ]_ R e. _V -> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R ) |
21 |
|
csbeq1a |
|- ( x = A -> R = [_ A / x ]_ R ) |
22 |
21
|
eleq1d |
|- ( x = A -> ( R e. _V <-> [_ A / x ]_ R e. _V ) ) |
23 |
|
oveq1 |
|- ( x = A -> ( x F y ) = ( A F y ) ) |
24 |
23 21
|
eqeq12d |
|- ( x = A -> ( ( x F y ) = R <-> ( A F y ) = [_ A / x ]_ R ) ) |
25 |
22 24
|
imbi12d |
|- ( x = A -> ( ( R e. _V -> ( x F y ) = R ) <-> ( [_ A / x ]_ R e. _V -> ( A F y ) = [_ A / x ]_ R ) ) ) |
26 |
|
csbeq1a |
|- ( y = B -> [_ A / x ]_ R = [_ B / y ]_ [_ A / x ]_ R ) |
27 |
26
|
eleq1d |
|- ( y = B -> ( [_ A / x ]_ R e. _V <-> [_ B / y ]_ [_ A / x ]_ R e. _V ) ) |
28 |
|
oveq2 |
|- ( y = B -> ( A F y ) = ( A F B ) ) |
29 |
28 26
|
eqeq12d |
|- ( y = B -> ( ( A F y ) = [_ A / x ]_ R <-> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R ) ) |
30 |
27 29
|
imbi12d |
|- ( y = B -> ( ( [_ A / x ]_ R e. _V -> ( A F y ) = [_ A / x ]_ R ) <-> ( [_ B / y ]_ [_ A / x ]_ R e. _V -> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R ) ) ) |
31 |
1
|
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 |
3 4 5 13 20 25 30 32
|
vtocl2gaf |
|- ( ( A e. C /\ B e. D ) -> ( [_ B / y ]_ [_ A / x ]_ R e. _V -> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R ) ) |
34 |
|
csbcom |
|- [_ A / x ]_ [_ B / y ]_ R = [_ B / y ]_ [_ A / x ]_ R |
35 |
34
|
eleq1i |
|- ( [_ A / x ]_ [_ B / y ]_ R e. _V <-> [_ B / y ]_ [_ A / x ]_ R e. _V ) |
36 |
34
|
eqeq2i |
|- ( ( A F B ) = [_ A / x ]_ [_ B / y ]_ R <-> ( A F B ) = [_ B / y ]_ [_ A / x ]_ R ) |
37 |
33 35 36
|
3imtr4g |
|- ( ( A e. C /\ B e. D ) -> ( [_ A / x ]_ [_ B / y ]_ R e. _V -> ( A F B ) = [_ A / x ]_ [_ B / y ]_ R ) ) |
38 |
2 37
|
syl5 |
|- ( ( A e. C /\ B e. D ) -> ( [_ A / x ]_ [_ B / y ]_ R e. V -> ( A F B ) = [_ A / x ]_ [_ B / y ]_ R ) ) |
39 |
38
|
3impia |
|- ( ( A e. C /\ B e. D /\ [_ A / x ]_ [_ B / y ]_ R e. V ) -> ( A F B ) = [_ A / x ]_ [_ B / y ]_ R ) |