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 |
|
relcnv |
|- Rel `' F |
7 |
|
nfcv |
|- F/_ y `' F |
8 |
3
|
nfcnv |
|- F/_ x `' F |
9 |
7 8
|
dffun6f |
|- ( Fun `' F <-> ( Rel `' F /\ A. y E* x y `' F x ) ) |
10 |
6 9
|
mpbiran |
|- ( Fun `' F <-> A. y E* x y `' F x ) |
11 |
|
vex |
|- y e. _V |
12 |
|
vex |
|- x e. _V |
13 |
11 12
|
brcnv |
|- ( y `' F x <-> x F y ) |
14 |
13
|
mobii |
|- ( E* x y `' F x <-> E* x x F y ) |
15 |
14
|
albii |
|- ( A. y E* x y `' F x <-> A. y E* x x F y ) |
16 |
10 15
|
bitri |
|- ( Fun `' F <-> A. y E* x x F y ) |
17 |
4
|
funmpt2 |
|- Fun F |
18 |
|
funbrfv2b |
|- ( Fun F -> ( x F y <-> ( x e. dom F /\ ( F ` x ) = y ) ) ) |
19 |
17 18
|
ax-mp |
|- ( x F y <-> ( x e. dom F /\ ( F ` x ) = y ) ) |
20 |
4
|
dmmpt |
|- dom F = { x e. A | B e. _V } |
21 |
5
|
elexd |
|- ( ( ph /\ x e. A ) -> B e. _V ) |
22 |
21
|
ex |
|- ( ph -> ( x e. A -> B e. _V ) ) |
23 |
1 22
|
ralrimi |
|- ( ph -> A. x e. A B e. _V ) |
24 |
2
|
rabid2f |
|- ( A = { x e. A | B e. _V } <-> A. x e. A B e. _V ) |
25 |
23 24
|
sylibr |
|- ( ph -> A = { x e. A | B e. _V } ) |
26 |
20 25
|
eqtr4id |
|- ( ph -> dom F = A ) |
27 |
26
|
eleq2d |
|- ( ph -> ( x e. dom F <-> x e. A ) ) |
28 |
27
|
anbi1d |
|- ( ph -> ( ( x e. dom F /\ ( F ` x ) = y ) <-> ( x e. A /\ ( F ` x ) = y ) ) ) |
29 |
19 28
|
syl5bb |
|- ( ph -> ( x F y <-> ( x e. A /\ ( F ` x ) = y ) ) ) |
30 |
29
|
bian1d |
|- ( ph -> ( ( x e. A /\ x F y ) <-> ( x e. A /\ ( F ` x ) = y ) ) ) |
31 |
|
simpr |
|- ( ( ph /\ x e. A ) -> x e. A ) |
32 |
4
|
fveq1i |
|- ( F ` x ) = ( ( x e. A |-> B ) ` x ) |
33 |
2
|
fvmpt2f |
|- ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B ) |
34 |
32 33
|
syl5eq |
|- ( ( x e. A /\ B e. V ) -> ( F ` x ) = B ) |
35 |
31 5 34
|
syl2anc |
|- ( ( ph /\ x e. A ) -> ( F ` x ) = B ) |
36 |
35
|
eqeq2d |
|- ( ( ph /\ x e. A ) -> ( y = ( F ` x ) <-> y = B ) ) |
37 |
|
eqcom |
|- ( ( F ` x ) = y <-> y = ( F ` x ) ) |
38 |
27
|
biimpar |
|- ( ( ph /\ x e. A ) -> x e. dom F ) |
39 |
|
funbrfvb |
|- ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) = y <-> x F y ) ) |
40 |
17 38 39
|
sylancr |
|- ( ( ph /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) ) |
41 |
37 40
|
bitr3id |
|- ( ( ph /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) ) |
42 |
36 41
|
bitr3d |
|- ( ( ph /\ x e. A ) -> ( y = B <-> x F y ) ) |
43 |
42
|
pm5.32da |
|- ( ph -> ( ( x e. A /\ y = B ) <-> ( x e. A /\ x F y ) ) ) |
44 |
30 43 29
|
3bitr4rd |
|- ( ph -> ( x F y <-> ( x e. A /\ y = B ) ) ) |
45 |
1 44
|
mobid |
|- ( ph -> ( E* x x F y <-> E* x ( x e. A /\ y = B ) ) ) |
46 |
|
df-rmo |
|- ( E* x e. A y = B <-> E* x ( x e. A /\ y = B ) ) |
47 |
45 46
|
bitr4di |
|- ( ph -> ( E* x x F y <-> E* x e. A y = B ) ) |
48 |
47
|
albidv |
|- ( ph -> ( A. y E* x x F y <-> A. y E* x e. A y = B ) ) |
49 |
16 48
|
syl5bb |
|- ( ph -> ( Fun `' F <-> A. y E* x e. A y = B ) ) |