Theorem xp1st 8006

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 5675	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3461	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3461	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7984	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2850	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 482	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 729	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1955	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ⟨cop 4591   × cxp 5650  ‘cfv 6525  1^st c1st 7972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fv 6533  df-1st 7974

This theorem is referenced by:  el2xptp0  8021  offval22  8071  mpof1o2d  8109  fimaproj  8119  xpf1o  9115  xpmapenlem  9120  mapunen  9122  unxpwdom2  9538  djulf1o  9886  djurf1o  9887  djur  9893  eldju1st  9897  r0weon  9984  infxpenlem  9985  fseqdom  9998  iundom2g  10512  enqbreq2  10893  nqereu  10902  addpqf  10917  mulpqf  10919  adderpqlem  10927  mulerpqlem  10928  addassnq  10931  mulassnq  10932  distrnq  10934  mulidnq  10936  recmulnq  10937  ltsonq  10942  lterpq  10943  ltanq  10944  ltmnq  10945  ltexnq  10948  archnq  10953  elreal2  11105  cnref1o  13000  fsum2dlem  15811  fsumcom2  15815  ackbijnn  15872  fprod2dlem  16024  fprodcom2  16028  ruclem6  16281  ruclem8  16283  ruclem9  16284  ruclem10  16285  ruclem11  16286  ruclem12  16287  eucalgval  16630  eucalginv  16632  eucalglt  16633  eucalg  16635  xpsff1o  17611  comfffval2  17747  comfeq  17752  idfucl  17928  funcpropd  17949  fucpropd  18027  xpccatid  18234  1stfcl  18243  2ndfcl  18244  xpcpropd  18254  hofcl  18305  hofpropd  18313  yonedalem3  18326  lsmhash  19766  gsum2dlem2  20032  evlslem4  22187  mdetunilem9  22738  tx2cn  23728  txdis  23750  txlly  23754  txnlly  23755  txhaus  23765  txkgen  23770  txconn  23807  txhmeo  23921  ptuncnv  23925  ptunhmeo  23926  xkohmeo  23933  utop2nei  24368  utop3cls  24369  imasdsf1olem  24491  cnheiborlem  25074  caubl  25428  caublcls  25429  bcthlem2  25445  bcthlem4  25447  bcthlem5  25448  ovolficcss  25589  ovoliunlem1  25622  ovoliunlem2  25623  ovolicc2lem1  25637  ovolicc2lem2  25638  ovolicc2lem4  25640  ovolicc2lem5  25641  dyadmbl  25720  fsumvma  27335  lgsquadlem1  27502  lgsquadlem2  27503  opreu2reuALT  32733  disjxpin  32843  fsumiunle  33086  gsummpt2d  33282  gsumwrd2dccatlem  33310  conjga  33403  elrgspnlem2  33476  elrgspnsubrunlem2  33481  erler  33498  rlocaddval  33502  rlocmulval  33503  mplvrpmga  33852  cnre2csqima  34218  tpr2rico  34219  esum2dlem  34399  esumiun  34401  2ndmbfm  34568  sxbrsigalem0  34578  dya2iocnrect  34588  sibfof  34647  sitgaddlemb  34655  hgt750lemb  34960  satefvfmla0  35781  msubff  35893  msubco  35894  mpst123  35903  msubvrs  35923  funtransport  36394  filnetlem3  36753  elxp8  37877  finixpnum  38116  poimirlem4  38135  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem9  38140  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem13  38144  poimirlem14  38145  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem25  38156  poimirlem26  38157  poimirlem27  38158  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  heicant  38166  mblfinlem1  38168  mblfinlem2  38169  ftc2nc  38213  heiborlem8  38329  dvhb1dimN  41622  dvhvaddcl  41731  dvhvaddcomN  41732  dvhvscacl  41739  dvhgrp  41743  dvhlveclem  41744  dibelval1st  41785  dicelval1stN  41824  aks6d1c2p1  42747  aks6d1c3  42752  aks6d1c4  42753  aks6d1c6lem2  42800  aks6d1c6lem4  42802  rmxypairf1o  43500  frmx  43502  cnmetcoval  45777  dvnprodlem1  46518  dvnprodlem2  46519  volicoff  46567  voliooicof  46568  etransclem44  46850  etransclem45  46851  etransclem47  46853  hoissre  47116  hoiprodcl  47119  ovnsubaddlem1  47142  ovnhoilem2  47174  hoicoto2  47177  ovncvr2  47183  opnvonmbllem2  47205  ovolval2lem  47215  ovolval3  47219  ovolval4lem1  47221  ovolval4lem2  47222  ovolval5lem2  47225  ovnovollem1  47228  ovnovollem2  47229  smfpimbor1lem1  47370  2arymaptf  49283  rrx2xpref1o  49349  elxpcbasex1ALT  49878  swapf2f1oa  49906  swapfida  49909  fuco2eld2  49943  fucoco2  49987  pgindlem  50344