Metamath Proof Explorer


Theorem df1stres

Description: Definition for a restriction of the 1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion df1stres 1 st A × B = x A , y B x

Proof

Step Hyp Ref Expression
1 df1st2 x y z | z = x = 1 st V × V
2 1 reseq1i x y z | z = x A × B = 1 st V × V A × B
3 resoprab x y z | z = x A × B = x y z | x A y B z = x
4 resres 1 st V × V A × B = 1 st V × V A × B
5 incom A × B V × V = V × V A × B
6 xpss A × B V × V
7 df-ss A × B V × V A × B V × V = A × B
8 6 7 mpbi A × B V × V = A × B
9 5 8 eqtr3i V × V A × B = A × B
10 9 reseq2i 1 st V × V A × B = 1 st A × B
11 4 10 eqtri 1 st V × V A × B = 1 st A × B
12 2 3 11 3eqtr3ri 1 st A × B = x y z | x A y B z = x
13 df-mpo x A , y B x = x y z | x A y B z = x
14 12 13 eqtr4i 1 st A × B = x A , y B x