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

Theorem xp1st 7703
 Description: Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
xp1st (𝐴 ∈ (𝐵 × 𝐶) → (1st𝐴) ∈ 𝐵)

Proof of Theorem xp1st
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp 5542 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)))
2 vex 3444 . . . . . . 7 𝑏 ∈ V
3 vex 3444 . . . . . . 7 𝑐 ∈ V
42, 3op1std 7681 . . . . . 6 (𝐴 = ⟨𝑏, 𝑐⟩ → (1st𝐴) = 𝑏)
54eleq1d 2874 . . . . 5 (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st𝐴) ∈ 𝐵𝑏𝐵))
65biimpar 481 . . . 4 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏𝐵) → (1st𝐴) ∈ 𝐵)
76adantrr 716 . . 3 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (1st𝐴) ∈ 𝐵)
87exlimivv 1933 . 2 (∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (1st𝐴) ∈ 𝐵)
91, 8sylbi 220 1 (𝐴 ∈ (𝐵 × 𝐶) → (1st𝐴) ∈ 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ⟨cop 4531   × cxp 5517  ‘cfv 6324  1st c1st 7669 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6283  df-fun 6326  df-fv 6332  df-1st 7671 This theorem is referenced by:  el2xptp0  7718  offval22  7766  fimaproj  7812  xpf1o  8663  xpmapenlem  8668  mapunen  8670  unxpwdom2  9036  djulf1o  9325  djurf1o  9326  djur  9332  eldju1st  9336  r0weon  9423  infxpenlem  9424  fseqdom  9437  iundom2g  9951  enqbreq2  10331  nqereu  10340  addpqf  10355  mulpqf  10357  adderpqlem  10365  mulerpqlem  10366  addassnq  10369  mulassnq  10370  distrnq  10372  mulidnq  10374  recmulnq  10375  ltsonq  10380  lterpq  10381  ltanq  10382  ltmnq  10383  ltexnq  10386  archnq  10391  elreal2  10543  cnref1o  12372  fsum2dlem  15117  fsumcom2  15121  ackbijnn  15175  fprod2dlem  15326  fprodcom2  15330  ruclem6  15580  ruclem8  15582  ruclem9  15583  ruclem10  15584  ruclem11  15585  ruclem12  15586  eucalgval  15916  eucalginv  15918  eucalglt  15919  eucalg  15921  xpsff1o  16832  comfffval2  16963  comfeq  16968  idfucl  17143  funcpropd  17162  fucpropd  17239  xpccatid  17430  1stfcl  17439  2ndfcl  17440  xpcpropd  17450  hofcl  17501  hofpropd  17509  yonedalem3  17522  lsmhash  18823  gsum2dlem2  19084  evlslem4  20747  mdetunilem9  21225  tx2cn  22215  txdis  22237  txlly  22241  txnlly  22242  txhaus  22252  txkgen  22257  txconn  22294  txhmeo  22408  ptuncnv  22412  ptunhmeo  22413  xkohmeo  22420  utop2nei  22856  utop3cls  22857  imasdsf1olem  22980  cnheiborlem  23559  caubl  23912  caublcls  23913  bcthlem2  23929  bcthlem4  23931  bcthlem5  23932  ovolficcss  24073  ovoliunlem1  24106  ovoliunlem2  24107  ovolicc2lem1  24121  ovolicc2lem2  24122  ovolicc2lem4  24124  ovolicc2lem5  24125  dyadmbl  24204  fsumvma  25797  lgsquadlem1  25964  lgsquadlem2  25965  opreu2reuALT  30247  disjxpin  30351  fsumiunle  30571  gsummpt2d  30734  cnre2csqima  31264  tpr2rico  31265  esum2dlem  31461  esumiun  31463  2ndmbfm  31629  sxbrsigalem0  31639  dya2iocnrect  31649  sibfof  31708  sitgaddlemb  31716  hgt750lemb  32037  satefvfmla0  32778  msubff  32890  msubco  32891  mpst123  32900  msubvrs  32920  funtransport  33605  filnetlem3  33841  elxp8  34788  finixpnum  35042  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem9  35066  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  heicant  35092  mblfinlem1  35094  mblfinlem2  35095  ftc2nc  35139  heiborlem8  35256  dvhb1dimN  38282  dvhvaddcl  38391  dvhvaddcomN  38392  dvhvscacl  38399  dvhgrp  38403  dvhlveclem  38404  dibelval1st  38445  dicelval1stN  38484  rmxypairf1o  39850  frmx  39852  cnmetcoval  41829  dvnprodlem1  42586  dvnprodlem2  42587  volicoff  42635  voliooicof  42636  etransclem44  42918  etransclem45  42919  etransclem47  42921  hoissre  43181  hoiprodcl  43184  ovnsubaddlem1  43207  ovnhoilem2  43239  hoicoto2  43242  ovncvr2  43248  opnvonmbllem2  43270  ovolval2lem  43280  ovolval3  43284  ovolval4lem1  43286  ovolval4lem2  43287  ovolval5lem2  43290  ovnovollem1  43293  ovnovollem2  43294  smfpimbor1lem1  43428  2arymaptf  45064  rrx2xpref1o  45130
 Copyright terms: Public domain W3C validator