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

Theorem xp1st 6781
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 4813 . 2  |-  ( A  e.  ( B  X.  C )  <->  E. b E. c ( A  = 
<. b ,  c >.  /\  ( b  e.  B  /\  c  e.  C
) ) )
2 vex 3025 . . . . . . 7  |-  b  e. 
_V
3 vex 3025 . . . . . . 7  |-  c  e. 
_V
42, 3op1std 6761 . . . . . 6  |-  ( A  =  <. b ,  c
>.  ->  ( 1st `  A
)  =  b )
54eleq1d 2490 . . . . 5  |-  ( A  =  <. b ,  c
>.  ->  ( ( 1st `  A )  e.  B  <->  b  e.  B ) )
65biimpar 487 . . . 4  |-  ( ( A  =  <. b ,  c >.  /\  b  e.  B )  ->  ( 1st `  A )  e.  B )
76adantrr 721 . . 3  |-  ( ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 1st `  A )  e.  B
)
87exlimivv 1771 . 2  |-  ( E. b E. c ( A  =  <. b ,  c >.  /\  (
b  e.  B  /\  c  e.  C )
)  ->  ( 1st `  A )  e.  B
)
91, 8sylbi 198 1  |-  ( A  e.  ( B  X.  C )  ->  ( 1st `  A )  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437   E.wex 1657    e. wcel 1872   <.cop 3947    X. cxp 4794   ` cfv 5544   1stc1st 6749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-iota 5508  df-fun 5546  df-fv 5552  df-1st 6751
This theorem is referenced by:  el2xptp0  6795  offval22  6830  xpf1o  7687  xpmapenlem  7692  mapunen  7694  unxpwdom2  8056  r0weon  8395  infxpenlem  8396  fseqdom  8408  iundom2g  8916  enqbreq2  9296  nqereu  9305  addpqf  9320  mulpqf  9322  adderpqlem  9330  mulerpqlem  9331  addassnq  9334  mulassnq  9335  distrnq  9337  mulidnq  9339  recmulnq  9340  ltsonq  9345  lterpq  9346  ltanq  9347  ltmnq  9348  ltexnq  9351  archnq  9356  elreal2  9507  cnref1o  11248  fsum2dlem  13774  fsumcom2  13778  ackbijnn  13829  fprod2dlem  13977  fprodcom2  13981  ruclem6  14230  ruclem8  14232  ruclem9  14233  ruclem10  14234  ruclem11  14235  ruclem12  14236  eucalgval  14484  eucalginv  14486  eucalglt  14487  eucalg  14489  xpsff1o  15417  comfffval2  15549  comfeq  15554  idfucl  15729  funcpropd  15748  fucpropd  15825  xpccatid  16016  1stfcl  16025  2ndfcl  16026  xpcpropd  16036  hofcl  16087  hofpropd  16095  yonedalem3  16108  lsmhash  17298  gsum2dlem2  17546  evlslem4  18674  mdetunilem9  19587  tx2cn  20567  txdis  20589  txlly  20593  txnlly  20594  txhaus  20604  txkgen  20609  txcon  20646  txhmeo  20760  ptuncnv  20764  ptunhmeo  20765  xkohmeo  20772  utop2nei  21207  utop3cls  21208  imasdsf1olem  21330  cnheiborlem  21924  caubl  22219  caublcls  22220  bcthlem2  22235  bcthlem4  22237  bcthlem5  22238  ovolficcss  22364  ovoliunlem1  22397  ovoliunlem2  22398  ovolicc2lem1  22412  ovolicc2lem2  22413  ovolicc2lem4OLD  22415  ovolicc2lem4  22416  ovolicc2lem5  22417  dyadmbl  22500  fsumvma  24083  lgsquadlem1  24224  lgsquadlem2  24225  disjxpin  28144  gsummpt2d  28495  fimaproj  28612  cnre2csqima  28669  tpr2rico  28670  esum2dlem  28865  esumiun  28867  2ndmbfm  29035  sxbrsigalem0  29045  dya2iocnrect  29055  sibfof  29125  sitgaddlemb  29133  msubff  30120  msubco  30121  mpst123  30130  msubvrs  30150  funtransport  30747  filnetlem3  30985  elxp8  31681  finixpnum  31837  poimirlem4  31851  poimirlem5  31852  poimirlem6  31853  poimirlem7  31854  poimirlem8  31855  poimirlem9  31856  poimirlem10  31857  poimirlem11  31858  poimirlem12  31859  poimirlem13  31860  poimirlem14  31861  poimirlem15  31862  poimirlem16  31863  poimirlem17  31864  poimirlem18  31865  poimirlem19  31866  poimirlem20  31867  poimirlem21  31868  poimirlem22  31869  poimirlem25  31872  poimirlem26  31873  poimirlem27  31874  poimirlem29  31876  poimirlem30  31877  poimirlem31  31878  poimirlem32  31879  heicant  31882  mblfinlem1  31884  mblfinlem2  31885  ftc2nc  31933  heiborlem8  32057  dvhb1dimN  34465  dvhvaddcl  34575  dvhvaddcomN  34576  dvhvscacl  34583  dvhgrp  34587  dvhlveclem  34588  dibelval1st  34629  dicelval1stN  34668  rmxypairf1o  35672  frmx  35674  dvnprodlem1  37704  dvnprodlem2  37705  etransclem44  38026  etransclem45  38027  etransclem47  38029  hoissre  38213  hoiprodcl  38216  ovnsubaddlem1  38239  ovnhoilem2  38271
  Copyright terms: Public domain W3C validator