Step |
Hyp |
Ref |
Expression |
1 |
|
df-mpt |
|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) } |
2 |
|
velsn |
|- ( y e. { B } <-> y = B ) |
3 |
2
|
anbi2i |
|- ( ( x e. A /\ y e. { B } ) <-> ( x e. A /\ y = B ) ) |
4 |
3
|
anbi2i |
|- ( ( z = <. x , y >. /\ ( x e. A /\ y e. { B } ) ) <-> ( z = <. x , y >. /\ ( x e. A /\ y = B ) ) ) |
5 |
4
|
2exbii |
|- ( E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. { B } ) ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y = B ) ) ) |
6 |
|
eliunxp |
|- ( z e. U_ x e. A ( { x } X. { B } ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. { B } ) ) ) |
7 |
|
elopab |
|- ( z e. { <. x , y >. | ( x e. A /\ y = B ) } <-> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y = B ) ) ) |
8 |
5 6 7
|
3bitr4i |
|- ( z e. U_ x e. A ( { x } X. { B } ) <-> z e. { <. x , y >. | ( x e. A /\ y = B ) } ) |
9 |
8
|
eqriv |
|- U_ x e. A ( { x } X. { B } ) = { <. x , y >. | ( x e. A /\ y = B ) } |
10 |
1 9
|
eqtr4i |
|- ( x e. A |-> B ) = U_ x e. A ( { x } X. { B } ) |