Theorem xp1st 7965

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.

Step	Hyp	Ref	Expression
1		elxp 5645	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3434	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3434	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7943	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2822	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 718	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1934	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 217	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ⟨cop 4574   × cxp 5620  ‘cfv 6490  1^st c1st 7931

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fv 6498  df-1st 7933

This theorem is referenced by:  el2xptp0  7980  offval22  8029  fimaproj  8076  xpf1o  9068  xpmapenlem  9073  mapunen  9075  unxpwdom2  9494  djulf1o  9825  djurf1o  9826  djur  9832  eldju1st  9836  r0weon  9923  infxpenlem  9924  fseqdom  9937  iundom2g  10451  enqbreq2  10832  nqereu  10841  addpqf  10856  mulpqf  10858  adderpqlem  10866  mulerpqlem  10867  addassnq  10870  mulassnq  10871  distrnq  10873  mulidnq  10875  recmulnq  10876  ltsonq  10881  lterpq  10882  ltanq  10883  ltmnq  10884  ltexnq  10887  archnq  10892  elreal2  11044  cnref1o  12924  fsum2dlem  15721  fsumcom2  15725  ackbijnn  15782  fprod2dlem  15934  fprodcom2  15938  ruclem6  16191  ruclem8  16193  ruclem9  16194  ruclem10  16195  ruclem11  16196  ruclem12  16197  eucalgval  16540  eucalginv  16542  eucalglt  16543  eucalg  16545  xpsff1o  17520  comfffval2  17656  comfeq  17661  idfucl  17837  funcpropd  17858  fucpropd  17936  xpccatid  18143  1stfcl  18152  2ndfcl  18153  xpcpropd  18163  hofcl  18214  hofpropd  18222  yonedalem3  18235  lsmhash  19669  gsum2dlem2  19935  evlslem4  22063  mdetunilem9  22594  tx2cn  23584  txdis  23606  txlly  23610  txnlly  23611  txhaus  23621  txkgen  23626  txconn  23663  txhmeo  23777  ptuncnv  23781  ptunhmeo  23782  xkohmeo  23789  utop2nei  24224  utop3cls  24225  imasdsf1olem  24347  cnheiborlem  24930  caubl  25284  caublcls  25285  bcthlem2  25301  bcthlem4  25303  bcthlem5  25304  ovolficcss  25445  ovoliunlem1  25478  ovoliunlem2  25479  ovolicc2lem1  25493  ovolicc2lem2  25494  ovolicc2lem4  25496  ovolicc2lem5  25497  dyadmbl  25576  fsumvma  27195  lgsquadlem1  27362  lgsquadlem2  27363  opreu2reuALT  32566  disjxpin  32678  fsumiunle  32922  gsummpt2d  33130  gsumwrd2dccatlem  33158  conjga  33251  elrgspnlem2  33324  elrgspnsubrunlem2  33329  erler  33346  rlocaddval  33349  rlocmulval  33350  mplvrpmga  33709  cnre2csqima  34076  tpr2rico  34077  esum2dlem  34257  esumiun  34259  2ndmbfm  34426  sxbrsigalem0  34436  dya2iocnrect  34446  sibfof  34505  sitgaddlemb  34513  hgt750lemb  34821  satefvfmla0  35621  msubff  35733  msubco  35734  mpst123  35743  msubvrs  35763  funtransport  36234  filnetlem3  36583  elxp8  37698  finixpnum  37937  poimirlem4  37956  poimirlem5  37957  poimirlem6  37958  poimirlem7  37959  poimirlem8  37960  poimirlem9  37961  poimirlem10  37962  poimirlem11  37963  poimirlem12  37964  poimirlem13  37965  poimirlem14  37966  poimirlem15  37967  poimirlem16  37968  poimirlem17  37969  poimirlem18  37970  poimirlem19  37971  poimirlem20  37972  poimirlem21  37973  poimirlem22  37974  poimirlem25  37977  poimirlem26  37978  poimirlem27  37979  poimirlem29  37981  poimirlem30  37982  poimirlem31  37983  poimirlem32  37984  heicant  37987  mblfinlem1  37989  mblfinlem2  37990  ftc2nc  38034  heiborlem8  38150  dvhb1dimN  41443  dvhvaddcl  41552  dvhvaddcomN  41553  dvhvscacl  41560  dvhgrp  41564  dvhlveclem  41565  dibelval1st  41606  dicelval1stN  41645  aks6d1c2p1  42568  aks6d1c3  42573  aks6d1c4  42574  aks6d1c6lem2  42621  aks6d1c6lem4  42623  f1o2d2  42685  rmxypairf1o  43354  frmx  43356  cnmetcoval  45646  dvnprodlem1  46389  dvnprodlem2  46390  volicoff  46438  voliooicof  46439  etransclem44  46721  etransclem45  46722  etransclem47  46724  hoissre  46987  hoiprodcl  46990  ovnsubaddlem1  47013  ovnhoilem2  47045  hoicoto2  47048  ovncvr2  47054  opnvonmbllem2  47076  ovolval2lem  47086  ovolval3  47090  ovolval4lem1  47092  ovolval4lem2  47093  ovolval5lem2  47096  ovnovollem1  47099  ovnovollem2  47100  smfpimbor1lem1  47241  2arymaptf  49125  rrx2xpref1o  49191  elxpcbasex1ALT  49721  swapf2f1oa  49749  swapfida  49752  fuco2eld2  49786  fucoco2  49830  pgindlem  50187