Metamath Proof Explorer


Theorem f1stres

Description: Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion f1stres 1stA×B:A×BA

Proof

Step Hyp Ref Expression
1 vex yV
2 vex zV
3 1 2 op1sta domyz=y
4 3 eleq1i domyzAyA
5 4 biimpri yAdomyzA
6 5 adantr yAzBdomyzA
7 6 rgen2 yAzBdomyzA
8 sneq x=yzx=yz
9 8 dmeqd x=yzdomx=domyz
10 9 unieqd x=yzdomx=domyz
11 10 eleq1d x=yzdomxAdomyzA
12 11 ralxp xA×BdomxAyAzBdomyzA
13 7 12 mpbir xA×BdomxA
14 df-1st 1st=xVdomx
15 14 reseq1i 1stA×B=xVdomxA×B
16 ssv A×BV
17 resmpt A×BVxVdomxA×B=xA×Bdomx
18 16 17 ax-mp xVdomxA×B=xA×Bdomx
19 15 18 eqtri 1stA×B=xA×Bdomx
20 19 fmpt xA×BdomxA1stA×B:A×BA
21 13 20 mpbi 1stA×B:A×BA