Step |
Hyp |
Ref |
Expression |
1 |
|
eqfnfv |
|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) ) |
2 |
|
eqcom |
|- ( { x e. A | ( F ` x ) = ( G ` x ) } = A <-> A = { x e. A | ( F ` x ) = ( G ` x ) } ) |
3 |
|
rabid2 |
|- ( A = { x e. A | ( F ` x ) = ( G ` x ) } <-> A. x e. A ( F ` x ) = ( G ` x ) ) |
4 |
2 3
|
bitri |
|- ( { x e. A | ( F ` x ) = ( G ` x ) } = A <-> A. x e. A ( F ` x ) = ( G ` x ) ) |
5 |
1 4
|
bitr4di |
|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> { x e. A | ( F ` x ) = ( G ` x ) } = A ) ) |
6 |
|
fndmin |
|- ( ( F Fn A /\ G Fn A ) -> dom ( F i^i G ) = { x e. A | ( F ` x ) = ( G ` x ) } ) |
7 |
6
|
eqeq1d |
|- ( ( F Fn A /\ G Fn A ) -> ( dom ( F i^i G ) = A <-> { x e. A | ( F ` x ) = ( G ` x ) } = A ) ) |
8 |
5 7
|
bitr4d |
|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> dom ( F i^i G ) = A ) ) |