Description: Express a singleton function in maps-to notation. (Contributed by NM, 6-Jun-2006) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by Stefan O'Rear, 28-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fmptsn | |- ( ( A e. V /\ B e. W ) -> { <. A , B >. } = ( x e. { A } |-> B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpsng | |- ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) = { <. A , B >. } ) |
|
| 2 | fconstmpt | |- ( { A } X. { B } ) = ( x e. { A } |-> B ) |
|
| 3 | 1 2 | eqtr3di | |- ( ( A e. V /\ B e. W ) -> { <. A , B >. } = ( x e. { A } |-> B ) ) |