Theorem xp1st 7967

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 5648	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3445	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3445	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7945	. . . . . 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 4587   × cxp 5623  ‘cfv 6493  1^st c1st 7933

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 5242  ax-nul 5252  ax-pr 5378  ax-un 7682

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fv 6501  df-1st 7935

This theorem is referenced by:  el2xptp0  7982  offval22  8032  fimaproj  8079  xpf1o  9071  xpmapenlem  9076  mapunen  9078  unxpwdom2  9497  djulf1o  9828  djurf1o  9829  djur  9835  eldju1st  9839  r0weon  9926  infxpenlem  9927  fseqdom  9940  iundom2g  10454  enqbreq2  10835  nqereu  10844  addpqf  10859  mulpqf  10861  adderpqlem  10869  mulerpqlem  10870  addassnq  10873  mulassnq  10874  distrnq  10876  mulidnq  10878  recmulnq  10879  ltsonq  10884  lterpq  10885  ltanq  10886  ltmnq  10887  ltexnq  10890  archnq  10895  elreal2  11047  cnref1o  12902  fsum2dlem  15697  fsumcom2  15701  ackbijnn  15755  fprod2dlem  15907  fprodcom2  15911  ruclem6  16164  ruclem8  16166  ruclem9  16167  ruclem10  16168  ruclem11  16169  ruclem12  16170  eucalgval  16513  eucalginv  16515  eucalglt  16516  eucalg  16518  xpsff1o  17492  comfffval2  17628  comfeq  17633  idfucl  17809  funcpropd  17830  fucpropd  17908  xpccatid  18115  1stfcl  18124  2ndfcl  18125  xpcpropd  18135  hofcl  18186  hofpropd  18194  yonedalem3  18207  lsmhash  19638  gsum2dlem2  19904  evlslem4  22035  mdetunilem9  22568  tx2cn  23558  txdis  23580  txlly  23584  txnlly  23585  txhaus  23595  txkgen  23600  txconn  23637  txhmeo  23751  ptuncnv  23755  ptunhmeo  23756  xkohmeo  23763  utop2nei  24198  utop3cls  24199  imasdsf1olem  24321  cnheiborlem  24913  caubl  25268  caublcls  25269  bcthlem2  25285  bcthlem4  25287  bcthlem5  25288  ovolficcss  25430  ovoliunlem1  25463  ovoliunlem2  25464  ovolicc2lem1  25478  ovolicc2lem2  25479  ovolicc2lem4  25481  ovolicc2lem5  25482  dyadmbl  25561  fsumvma  27184  lgsquadlem1  27351  lgsquadlem2  27352  opreu2reuALT  32533  disjxpin  32645  fsumiunle  32891  gsummpt2d  33113  gsumwrd2dccatlem  33140  conjga  33233  elrgspnlem2  33306  elrgspnsubrunlem2  33311  erler  33328  rlocaddval  33331  rlocmulval  33332  mplvrpmga  33691  cnre2csqima  34049  tpr2rico  34050  esum2dlem  34230  esumiun  34232  2ndmbfm  34399  sxbrsigalem0  34409  dya2iocnrect  34419  sibfof  34478  sitgaddlemb  34486  hgt750lemb  34794  satefvfmla0  35593  msubff  35705  msubco  35706  mpst123  35715  msubvrs  35735  funtransport  36206  filnetlem3  36555  elxp8  37547  finixpnum  37777  poimirlem4  37796  poimirlem5  37797  poimirlem6  37798  poimirlem7  37799  poimirlem8  37800  poimirlem9  37801  poimirlem10  37802  poimirlem11  37803  poimirlem12  37804  poimirlem13  37805  poimirlem14  37806  poimirlem15  37807  poimirlem16  37808  poimirlem17  37809  poimirlem18  37810  poimirlem19  37811  poimirlem20  37812  poimirlem21  37813  poimirlem22  37814  poimirlem25  37817  poimirlem26  37818  poimirlem27  37819  poimirlem29  37821  poimirlem30  37822  poimirlem31  37823  poimirlem32  37824  heicant  37827  mblfinlem1  37829  mblfinlem2  37830  ftc2nc  37874  heiborlem8  37990  dvhb1dimN  41283  dvhvaddcl  41392  dvhvaddcomN  41393  dvhvscacl  41400  dvhgrp  41404  dvhlveclem  41405  dibelval1st  41446  dicelval1stN  41485  aks6d1c2p1  42409  aks6d1c3  42414  aks6d1c4  42415  aks6d1c6lem2  42462  aks6d1c6lem4  42464  f1o2d2  42526  rmxypairf1o  43189  frmx  43191  cnmetcoval  45482  dvnprodlem1  46226  dvnprodlem2  46227  volicoff  46275  voliooicof  46276  etransclem44  46558  etransclem45  46559  etransclem47  46561  hoissre  46824  hoiprodcl  46827  ovnsubaddlem1  46850  ovnhoilem2  46882  hoicoto2  46885  ovncvr2  46891  opnvonmbllem2  46913  ovolval2lem  46923  ovolval3  46927  ovolval4lem1  46929  ovolval4lem2  46930  ovolval5lem2  46933  ovnovollem1  46936  ovnovollem2  46937  smfpimbor1lem1  47078  2arymaptf  48934  rrx2xpref1o  49000  elxpcbasex1ALT  49530  swapf2f1oa  49558  swapfida  49561  fuco2eld2  49595  fucoco2  49639  pgindlem  49996