This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfmpt3

Description: Alternate definition for the maps-to notation df-mpt . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Assertion dfmpt3 
|- ( x e. A |-> B ) = U_ x e. A ( { x } X. { B } )

Proof

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 } )