Step |
Hyp |
Ref |
Expression |
1 |
|
funcnvmpt.0 |
|- F/ x ph |
2 |
|
funcnvmpt.1 |
|- F/_ x A |
3 |
|
funcnvmpt.2 |
|- F/_ x F |
4 |
|
funcnvmpt.3 |
|- F = ( x e. A |-> B ) |
5 |
|
funcnvmpt.4 |
|- ( ( ph /\ x e. A ) -> B e. V ) |
6 |
|
nfv |
|- F/ i ph |
7 |
|
nfcv |
|- F/_ i A |
8 |
|
nfcv |
|- F/_ i F |
9 |
|
nfcv |
|- F/_ i B |
10 |
|
nfcsb1v |
|- F/_ x [_ i / x ]_ B |
11 |
|
csbeq1a |
|- ( x = i -> B = [_ i / x ]_ B ) |
12 |
2 7 9 10 11
|
cbvmptf |
|- ( x e. A |-> B ) = ( i e. A |-> [_ i / x ]_ B ) |
13 |
4 12
|
eqtri |
|- F = ( i e. A |-> [_ i / x ]_ B ) |
14 |
5
|
sbimi |
|- ( [ i / x ] ( ph /\ x e. A ) -> [ i / x ] B e. V ) |
15 |
|
nfcv |
|- F/_ x i |
16 |
15 2
|
nfel |
|- F/ x i e. A |
17 |
1 16
|
nfan |
|- F/ x ( ph /\ i e. A ) |
18 |
|
eleq1w |
|- ( x = i -> ( x e. A <-> i e. A ) ) |
19 |
18
|
anbi2d |
|- ( x = i -> ( ( ph /\ x e. A ) <-> ( ph /\ i e. A ) ) ) |
20 |
17 19
|
sbiev |
|- ( [ i / x ] ( ph /\ x e. A ) <-> ( ph /\ i e. A ) ) |
21 |
|
nfcv |
|- F/_ x V |
22 |
10 21
|
nfel |
|- F/ x [_ i / x ]_ B e. V |
23 |
11
|
eleq1d |
|- ( x = i -> ( B e. V <-> [_ i / x ]_ B e. V ) ) |
24 |
22 23
|
sbiev |
|- ( [ i / x ] B e. V <-> [_ i / x ]_ B e. V ) |
25 |
14 20 24
|
3imtr3i |
|- ( ( ph /\ i e. A ) -> [_ i / x ]_ B e. V ) |
26 |
|
csbeq1 |
|- ( i = j -> [_ i / x ]_ B = [_ j / x ]_ B ) |
27 |
6 7 8 13 25 26
|
funcnv5mpt |
|- ( ph -> ( Fun `' F <-> A. i e. A A. j e. A ( i = j \/ [_ i / x ]_ B =/= [_ j / x ]_ B ) ) ) |