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

Theorem xp1st 7582
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 5471 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)))
2 vex 3440 . . . . . . 7 𝑏 ∈ V
3 vex 3440 . . . . . . 7 𝑐 ∈ V
42, 3op1std 7560 . . . . . 6 (𝐴 = ⟨𝑏, 𝑐⟩ → (1st𝐴) = 𝑏)
54eleq1d 2867 . . . . 5 (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st𝐴) ∈ 𝐵𝑏𝐵))
65biimpar 478 . . . 4 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏𝐵) → (1st𝐴) ∈ 𝐵)
76adantrr 713 . . 3 ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (1st𝐴) ∈ 𝐵)
87exlimivv 1910 . 2 (∃𝑏𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏𝐵𝑐𝐶)) → (1st𝐴) ∈ 𝐵)
91, 8sylbi 218 1 (𝐴 ∈ (𝐵 × 𝐶) → (1st𝐴) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wex 1761  wcel 2081  cop 4482   × cxp 5446  cfv 6230  1st c1st 7548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-iota 6194  df-fun 6232  df-fv 6238  df-1st 7550
This theorem is referenced by:  el2xptp0  7597  offval22  7644  xpf1o  8531  xpmapenlem  8536  mapunen  8538  unxpwdom2  8903  djulf1o  9192  djurf1o  9193  djur  9199  eldju1st  9203  r0weon  9289  infxpenlem  9290  fseqdom  9303  iundom2g  9813  enqbreq2  10193  nqereu  10202  addpqf  10217  mulpqf  10219  adderpqlem  10227  mulerpqlem  10228  addassnq  10231  mulassnq  10232  distrnq  10234  mulidnq  10236  recmulnq  10237  ltsonq  10242  lterpq  10243  ltanq  10244  ltmnq  10245  ltexnq  10248  archnq  10253  elreal2  10405  cnref1o  12239  fsum2dlem  14963  fsumcom2  14967  ackbijnn  15021  fprod2dlem  15172  fprodcom2  15176  ruclem6  15426  ruclem8  15428  ruclem9  15429  ruclem10  15430  ruclem11  15431  ruclem12  15432  eucalgval  15760  eucalginv  15762  eucalglt  15763  eucalg  15765  xpsff1o  16674  comfffval2  16805  comfeq  16810  idfucl  16985  funcpropd  17004  fucpropd  17081  xpccatid  17272  1stfcl  17281  2ndfcl  17282  xpcpropd  17292  hofcl  17343  hofpropd  17351  yonedalem3  17364  lsmhash  18563  gsum2dlem2  18816  evlslem4  19980  mdetunilem9  20918  tx2cn  21907  txdis  21929  txlly  21933  txnlly  21934  txhaus  21944  txkgen  21949  txconn  21986  txhmeo  22100  ptuncnv  22104  ptunhmeo  22105  xkohmeo  22112  utop2nei  22547  utop3cls  22548  imasdsf1olem  22671  cnheiborlem  23246  caubl  23599  caublcls  23600  bcthlem2  23616  bcthlem4  23618  bcthlem5  23619  ovolficcss  23758  ovoliunlem1  23791  ovoliunlem2  23792  ovolicc2lem1  23806  ovolicc2lem2  23807  ovolicc2lem4  23809  ovolicc2lem5  23810  dyadmbl  23889  fsumvma  25476  lgsquadlem1  25643  lgsquadlem2  25644  opreu2reuALT  29937  disjxpin  30033  fsumiunle  30234  gsummpt2d  30501  fimaproj  30719  cnre2csqima  30776  tpr2rico  30777  esum2dlem  30973  esumiun  30975  2ndmbfm  31141  sxbrsigalem0  31151  dya2iocnrect  31161  sibfof  31220  sitgaddlemb  31228  hgt750lemb  31549  satefvfmla0  32279  msubff  32391  msubco  32392  mpst123  32401  msubvrs  32421  funtransport  33107  filnetlem3  33343  elxp8  34208  finixpnum  34433  poimirlem4  34452  poimirlem5  34453  poimirlem6  34454  poimirlem7  34455  poimirlem8  34456  poimirlem9  34457  poimirlem10  34458  poimirlem11  34459  poimirlem12  34460  poimirlem13  34461  poimirlem14  34462  poimirlem15  34463  poimirlem16  34464  poimirlem17  34465  poimirlem18  34466  poimirlem19  34467  poimirlem20  34468  poimirlem21  34469  poimirlem22  34470  poimirlem25  34473  poimirlem26  34474  poimirlem27  34475  poimirlem29  34477  poimirlem30  34478  poimirlem31  34479  poimirlem32  34480  heicant  34483  mblfinlem1  34485  mblfinlem2  34486  ftc2nc  34532  heiborlem8  34653  dvhb1dimN  37678  dvhvaddcl  37787  dvhvaddcomN  37788  dvhvscacl  37795  dvhgrp  37799  dvhlveclem  37800  dibelval1st  37841  dicelval1stN  37880  rmxypairf1o  39018  frmx  39020  cnmetcoval  41030  dvnprodlem1  41798  dvnprodlem2  41799  volicoff  41848  voliooicof  41849  etransclem44  42131  etransclem45  42132  etransclem47  42134  hoissre  42394  hoiprodcl  42397  ovnsubaddlem1  42420  ovnhoilem2  42452  hoicoto2  42455  ovncvr2  42461  opnvonmbllem2  42483  ovolval2lem  42493  ovolval3  42497  ovolval4lem1  42499  ovolval4lem2  42500  ovolval5lem2  42503  ovnovollem1  42506  ovnovollem2  42507  smfpimbor1lem1  42641  rrx2xpref1o  44212
  Copyright terms: Public domain W3C validator