Theorem xp1st 6220

Description: Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
xp1st	|- ( A e. ( B X. C ) -> ( 1st ` A ) e. B )

Proof of Theorem xp1st

Dummy variables b c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 4677	. 2 |- ( A e. ( B X. C ) <-> E. b E. c ( A = <. b , c >. /\ ( b e. B /\ c e. C ) ) )
2		vex 2763	. . . . . . 7 |- b e. _V
3		vex 2763	. . . . . . 7 |- c e. _V
4	2, 3	op1std 6203	. . . . . 6 |- ( A = <. b , c >. -> ( 1st ` A ) = b )
5	4	eleq1d 2262	. . . . 5 |- ( A = <. b , c >. -> ( ( 1st ` A ) e. B <-> b e. B ) )
6	5	biimpar 297	. . . 4 |- ( ( A = <. b , c >. /\ b e. B ) -> ( 1st ` A ) e. B )
7	6	adantrr 479	. . 3 |- ( ( A = <. b , c >. /\ ( b e. B /\ c e. C ) ) -> ( 1st ` A ) e. B )
8	7	exlimivv 1908	. 2 |- ( E. b E. c ( A = <. b , c >. /\ ( b e. B /\ c e. C ) ) -> ( 1st ` A ) e. B )
9	1, 8	sylbi 121	1 |- ( A e. ( B X. C ) -> ( 1st ` A ) e. B )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   E.wex 1503   e. wcel 2164   <.cop 3622   X. cxp 4658   ` cfv 5255   1stc1st 6193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-sbc 2987  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-opab 4092  df-mpt 4093  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-rn 4671  df-iota 5216  df-fun 5257  df-fv 5263  df-1st 6195

This theorem is referenced by:  disjxp1  6291  xpf1o  6902  xpmapenlem  6907  opabfi  6994  djuf1olem  7114  eldju1st  7132  exmidapne  7322  dfplpq2  7416  dfmpq2  7417  enqbreq2  7419  enqdc1  7424  mulpipq2  7433  preqlu  7534  elnp1st2nd  7538  cauappcvgprlemladd  7720  elreal2  7892  cnref1o  9719  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgsuctlem  10497  seq3val  10534  seqvalcd  10535  fsum2dlemstep  11580  fisumcom2  11584  fprod2dlemstep  11768  fprodcom2fi  11772  eucalgval  12195  eucalginv  12197  eucalglt  12198  eucalg  12200  sqpweven  12316  2sqpwodd  12317  ctiunctlemudc  12597  xpsff1o  12935  tx2cn  14449  txdis  14456  txhmeo  14498  xmetxp  14686  xmetxpbl  14687  xmettxlem  14688  xmettx  14689  lgsquadlemofi  15233  lgsquadlem1  15234  lgsquadlem2  15235