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

Theorem xp1st 6729
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 4930 . 2  |-  ( A  e.  ( B  X.  C )  <->  E. b E. c ( A  = 
<. b ,  c >.  /\  ( b  e.  B  /\  c  e.  C
) ) )
2 vex 3037 . . . . . . 7  |-  b  e. 
_V
3 vex 3037 . . . . . . 7  |-  c  e. 
_V
42, 3op1std 6709 . . . . . 6  |-  ( A  =  <. b ,  c
>.  ->  ( 1st `  A
)  =  b )
54eleq1d 2451 . . . . 5  |-  ( A  =  <. b ,  c
>.  ->  ( ( 1st `  A )  e.  B  <->  b  e.  B ) )
65biimpar 483 . . . 4  |-  ( ( A  =  <. b ,  c >.  /\  b  e.  B )  ->  ( 1st `  A )  e.  B )
76adantrr 714 . . 3  |-  ( ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 1st `  A )  e.  B
)
87exlimivv 1731 . 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 367    = wceq 1399   E.wex 1620    e. wcel 1826   <.cop 3950    X. cxp 4911   ` cfv 5496   1stc1st 6697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-iota 5460  df-fun 5498  df-fv 5504  df-1st 6699
This theorem is referenced by:  el2xptp0  6743  offval22  6778  xpf1o  7598  xpmapenlem  7603  mapunen  7605  unxpwdom2  7929  r0weon  8303  infxpenlem  8304  fseqdom  8320  iundom2g  8828  enqbreq2  9209  nqereu  9218  addpqf  9233  mulpqf  9235  adderpqlem  9243  mulerpqlem  9244  addassnq  9247  mulassnq  9248  distrnq  9250  mulidnq  9252  recmulnq  9253  ltsonq  9258  lterpq  9259  ltanq  9260  ltmnq  9261  ltexnq  9264  archnq  9269  elreal2  9420  cnref1o  11134  fsum2dlem  13587  fsumcom2  13591  ackbijnn  13642  fprod2dlem  13786  fprodcom2  13790  ruclem6  13970  ruclem8  13972  ruclem9  13973  ruclem10  13974  ruclem11  13975  ruclem12  13976  eucalgval  14213  eucalginv  14215  eucalglt  14216  eucalg  14218  xpsff1o  14975  comfffval2  15107  comfeq  15112  idfucl  15287  funcpropd  15306  fucpropd  15383  xpccatid  15574  1stfcl  15583  2ndfcl  15584  xpcpropd  15594  hofcl  15645  hofpropd  15653  yonedalem3  15666  lsmhash  16840  gsum2dlem2  17112  gsum2dOLD  17114  evlslem4OLD  18286  evlslem4  18287  mdetunilem9  19207  tx2cn  20196  txdis  20218  txlly  20222  txnlly  20223  txhaus  20233  txkgen  20238  txcon  20275  txhmeo  20389  ptuncnv  20393  ptunhmeo  20394  xkohmeo  20401  utop2nei  20838  utop3cls  20839  imasdsf1olem  20961  cnheiborlem  21539  caubl  21831  caublcls  21832  bcthlem2  21849  bcthlem4  21851  bcthlem5  21852  ovolficcss  21966  ovoliunlem1  21998  ovoliunlem2  21999  ovolicc2lem1  22013  ovolicc2lem2  22014  ovolicc2lem4  22016  ovolicc2lem5  22017  dyadmbl  22094  fsumvma  23605  lgsquadlem1  23746  lgsquadlem2  23747  disjxpin  27577  gsummpt2d  27925  fimaproj  27990  cnre2csqima  28047  tpr2rico  28048  esum2dlem  28240  esumiun  28242  2ndmbfm  28388  sxbrsigalem0  28398  dya2iocnrect  28408  sibfof  28465  msubff  29079  msubco  29080  mpst123  29089  msubvrs  29109  funtransport  29834  finixpnum  30203  heicant  30214  mblfinlem1  30216  mblfinlem2  30217  ftc2nc  30265  filnetlem3  30364  heiborlem8  30480  rmxypairf1o  31012  frmx  31014  dvnprodlem1  31909  dvnprodlem2  31910  etransclem44  32227  etransclem45  32228  etransclem47  32230  dvhb1dimN  37125  dvhvaddcl  37235  dvhvaddcomN  37236  dvhvscacl  37243  dvhgrp  37247  dvhlveclem  37248  dibelval1st  37289  dicelval1stN  37328
  Copyright terms: Public domain W3C validator