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 A × B | F 1 st x = 2 nd x

Proof

Step Hyp Ref Expression
1 fgraphopab F : A B F = a b | a A b B F a = b
2 vex a V
3 vex b V
4 2 3 op1std x = a b 1 st x = a
5 4 fveq2d x = a b F 1 st x = F a
6 2 3 op2ndd x = a b 2 nd x = b
7 5 6 eqeq12d x = a b F 1 st x = 2 nd x F a = b
8 7 rabxp x A × B | F 1 st x = 2 nd x = a b | a A b B F a = b
9 df-3an a A b B F a = b a A b B F a = b
10 9 opabbii a b | a A b B F a = b = a b | a A b B F a = b
11 8 10 eqtri x A × B | F 1 st x = 2 nd x = a b | a A b B F a = b
12 1 11 eqtr4di F : A B F = x A × B | F 1 st x = 2 nd x