Metamath Proof Explorer

Theorem fgraphxp

Description: Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion fgraphxp 
|- ( F : A --> B -> F = { x e. ( A X. B ) | ( F ` ( 1st ` x ) ) = ( 2nd ` x ) } )

Proof

Step Hyp Ref Expression
1 fgraphopab 
 |-  ( F : A --> B -> F = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) } )
2 vex 
 |-  a e. _V
3 vex 
 |-  b e. _V
4 2 3 op1std 
 |-  ( x = <. a , b >. -> ( 1st ` x ) = a )
5 4 fveq2d 
 |-  ( x = <. a , b >. -> ( F ` ( 1st ` x ) ) = ( F ` a ) )
6 2 3 op2ndd 
 |-  ( x = <. a , b >. -> ( 2nd ` x ) = b )
7 5 6 eqeq12d 
 |-  ( x = <. a , b >. -> ( ( F ` ( 1st ` x ) ) = ( 2nd ` x ) <-> ( F ` a ) = b ) )
8 7 rabxp 
 |-  { x e. ( A X. B ) | ( F ` ( 1st ` x ) ) = ( 2nd ` x ) } = { <. a , b >. | ( a e. A /\ b e. B /\ ( F ` a ) = b ) }
9 df-3an 
 |-  ( ( a e. A /\ b e. B /\ ( F ` a ) = b ) <-> ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) )
10 9 opabbii 
 |-  { <. a , b >. | ( a e. A /\ b e. B /\ ( F ` a ) = b ) } = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) }
11 8 10 eqtri 
 |-  { x e. ( A X. B ) | ( F ` ( 1st ` x ) ) = ( 2nd ` x ) } = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) }
12 1 11 eqtr4di 
 |-  ( F : A --> B -> F = { x e. ( A X. B ) | ( F ` ( 1st ` x ) ) = ( 2nd ` x ) } )