Theorem xp1st 7849

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 5611	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3434	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3434	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7827	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2824	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 713	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1938	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1785   ∈ wcel 2109  ⟨cop 4572   × cxp 5586  ‘cfv 6430  1^st c1st 7815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-iota 6388  df-fun 6432  df-fv 6438  df-1st 7817

This theorem is referenced by:  el2xptp0  7864  offval22  7912  fimaproj  7960  xpf1o  8891  xpmapenlem  8896  mapunen  8898  unxpwdom2  9308  djulf1o  9654  djurf1o  9655  djur  9661  eldju1st  9665  r0weon  9752  infxpenlem  9753  fseqdom  9766  iundom2g  10280  enqbreq2  10660  nqereu  10669  addpqf  10684  mulpqf  10686  adderpqlem  10694  mulerpqlem  10695  addassnq  10698  mulassnq  10699  distrnq  10701  mulidnq  10703  recmulnq  10704  ltsonq  10709  lterpq  10710  ltanq  10711  ltmnq  10712  ltexnq  10715  archnq  10720  elreal2  10872  cnref1o  12707  fsum2dlem  15463  fsumcom2  15467  ackbijnn  15521  fprod2dlem  15671  fprodcom2  15675  ruclem6  15925  ruclem8  15927  ruclem9  15928  ruclem10  15929  ruclem11  15930  ruclem12  15931  eucalgval  16268  eucalginv  16270  eucalglt  16271  eucalg  16273  xpsff1o  17259  comfffval2  17391  comfeq  17396  idfucl  17577  funcpropd  17597  fucpropd  17676  xpccatid  17886  1stfcl  17895  2ndfcl  17896  xpcpropd  17907  hofcl  17958  hofpropd  17966  yonedalem3  17979  lsmhash  19292  gsum2dlem2  19553  evlslem4  21265  mdetunilem9  21750  tx2cn  22742  txdis  22764  txlly  22768  txnlly  22769  txhaus  22779  txkgen  22784  txconn  22821  txhmeo  22935  ptuncnv  22939  ptunhmeo  22940  xkohmeo  22947  utop2nei  23383  utop3cls  23384  imasdsf1olem  23507  cnheiborlem  24098  caubl  24453  caublcls  24454  bcthlem2  24470  bcthlem4  24472  bcthlem5  24473  ovolficcss  24614  ovoliunlem1  24647  ovoliunlem2  24648  ovolicc2lem1  24662  ovolicc2lem2  24663  ovolicc2lem4  24665  ovolicc2lem5  24666  dyadmbl  24745  fsumvma  26342  lgsquadlem1  26509  lgsquadlem2  26510  opreu2reuALT  30804  disjxpin  30906  fsumiunle  31122  gsummpt2d  31288  cnre2csqima  31840  tpr2rico  31841  esum2dlem  32039  esumiun  32041  2ndmbfm  32207  sxbrsigalem0  32217  dya2iocnrect  32227  sibfof  32286  sitgaddlemb  32294  hgt750lemb  32615  satefvfmla0  33359  msubff  33471  msubco  33472  mpst123  33481  msubvrs  33501  funtransport  34312  filnetlem3  34548  elxp8  35521  finixpnum  35741  poimirlem4  35760  poimirlem5  35761  poimirlem6  35762  poimirlem7  35763  poimirlem8  35764  poimirlem9  35765  poimirlem10  35766  poimirlem11  35767  poimirlem12  35768  poimirlem13  35769  poimirlem14  35770  poimirlem15  35771  poimirlem16  35772  poimirlem17  35773  poimirlem18  35774  poimirlem19  35775  poimirlem20  35776  poimirlem21  35777  poimirlem22  35778  poimirlem25  35781  poimirlem26  35782  poimirlem27  35783  poimirlem29  35785  poimirlem30  35786  poimirlem31  35787  poimirlem32  35788  heicant  35791  mblfinlem1  35793  mblfinlem2  35794  ftc2nc  35838  heiborlem8  35955  dvhb1dimN  38979  dvhvaddcl  39088  dvhvaddcomN  39089  dvhvscacl  39096  dvhgrp  39100  dvhlveclem  39101  dibelval1st  39142  dicelval1stN  39181  rmxypairf1o  40713  frmx  40715  cnmetcoval  42695  dvnprodlem1  43441  dvnprodlem2  43442  volicoff  43490  voliooicof  43491  etransclem44  43773  etransclem45  43774  etransclem47  43776  hoissre  44036  hoiprodcl  44039  ovnsubaddlem1  44062  ovnhoilem2  44094  hoicoto2  44097  ovncvr2  44103  opnvonmbllem2  44125  ovolval2lem  44135  ovolval3  44139  ovolval4lem1  44141  ovolval4lem2  44142  ovolval5lem2  44145  ovnovollem1  44148  ovnovollem2  44149  smfpimbor1lem1  44283  2arymaptf  45950  rrx2xpref1o  46016