MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xp1st Structured version   Unicode version

Theorem xp1st 6811
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.
StepHypRef Expression
1 elxp 5016 . 2  |-  ( A  e.  ( B  X.  C )  <->  E. b E. c ( A  = 
<. b ,  c >.  /\  ( b  e.  B  /\  c  e.  C
) ) )
2 vex 3116 . . . . . . 7  |-  b  e. 
_V
3 vex 3116 . . . . . . 7  |-  c  e. 
_V
42, 3op1std 6791 . . . . . 6  |-  ( A  =  <. b ,  c
>.  ->  ( 1st `  A
)  =  b )
54eleq1d 2536 . . . . 5  |-  ( A  =  <. b ,  c
>.  ->  ( ( 1st `  A )  e.  B  <->  b  e.  B ) )
65biimpar 485 . . . 4  |-  ( ( A  =  <. b ,  c >.  /\  b  e.  B )  ->  ( 1st `  A )  e.  B )
76adantrr 716 . . 3  |-  ( ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 1st `  A )  e.  B
)
87exlimivv 1699 . 2  |-  ( E. b E. c ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 1st `  A )  e.  B
)
91, 8sylbi 195 1  |-  ( A  e.  ( B  X.  C )  ->  ( 1st `  A )  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379   E.wex 1596    e. wcel 1767   <.cop 4033    X. cxp 4997   ` cfv 5586   1stc1st 6779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-iota 5549  df-fun 5588  df-fv 5594  df-1st 6781
This theorem is referenced by:  el2xptp0  6825  offval22  6859  xpf1o  7676  xpmapenlem  7681  mapunen  7683  unxpwdom2  8010  r0weon  8386  infxpenlem  8387  fseqdom  8403  iundom2g  8911  enqbreq2  9294  nqereu  9303  addpqf  9318  mulpqf  9320  adderpqlem  9328  mulerpqlem  9329  addassnq  9332  mulassnq  9333  distrnq  9335  mulidnq  9337  recmulnq  9338  ltsonq  9343  lterpq  9344  ltanq  9345  ltmnq  9346  ltexnq  9349  archnq  9354  elreal2  9505  cnref1o  11211  fsum2dlem  13544  fsumcom2  13548  ackbijnn  13599  ruclem6  13825  ruclem8  13827  ruclem9  13828  ruclem10  13829  ruclem11  13830  ruclem12  13831  eucalgval  14066  eucalginv  14068  eucalglt  14069  eucalg  14071  xpsff1o  14819  comfffval2  14953  comfeq  14958  idfucl  15104  funcpropd  15123  fucpropd  15200  xpccatid  15311  1stfcl  15320  2ndfcl  15321  xpcpropd  15331  hofcl  15382  hofpropd  15390  yonedalem3  15403  lsmhash  16519  gsum2dlem2  16789  gsum2dOLD  16791  evlslem4OLD  17944  evlslem4  17945  mdetunilem9  18889  tx2cn  19846  txdis  19868  txlly  19872  txnlly  19873  txhaus  19883  txkgen  19888  txcon  19925  txhmeo  20039  ptuncnv  20043  ptunhmeo  20044  xkohmeo  20051  utop2nei  20488  utop3cls  20489  imasdsf1olem  20611  cnheiborlem  21189  caubl  21481  caublcls  21482  bcthlem2  21499  bcthlem4  21501  bcthlem5  21502  ovolficcss  21616  ovoliunlem1  21648  ovoliunlem2  21649  ovolicc2lem1  21663  ovolicc2lem2  21664  ovolicc2lem4  21666  ovolicc2lem5  21667  dyadmbl  21744  fsumvma  23216  lgsquadlem1  23357  lgsquadlem2  23358  disjxpin  27120  fimaproj  27499  cnre2csqima  27529  tpr2rico  27530  2ndmbfm  27872  sxbrsigalem0  27882  dya2iocnrect  27892  sibfof  27922  fprod2dlem  28687  fprodcom2  28691  funtransport  29258  finixpnum  29615  heicant  29626  mblfinlem1  29628  mblfinlem2  29629  ftc2nc  29676  filnetlem3  29801  heiborlem8  29917  rmxypairf1o  30451  frmx  30453  dvhb1dimN  35782  dvhvaddcl  35892  dvhvaddcomN  35893  dvhvscacl  35900  dvhgrp  35904  dvhlveclem  35905  dibelval1st  35946  dicelval1stN  35985
  Copyright terms: Public domain W3C validator