Theorem xp1st 8046

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 5708	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3484	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3484	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 8024	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2826	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 717	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1932	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 217	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ⟨cop 4632   × cxp 5683  ‘cfv 6561  1^st c1st 8012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014

This theorem is referenced by:  el2xptp0  8061  offval22  8113  fimaproj  8160  xpf1o  9179  xpmapenlem  9184  mapunen  9186  unxpwdom2  9628  djulf1o  9952  djurf1o  9953  djur  9959  eldju1st  9963  r0weon  10052  infxpenlem  10053  fseqdom  10066  iundom2g  10580  enqbreq2  10960  nqereu  10969  addpqf  10984  mulpqf  10986  adderpqlem  10994  mulerpqlem  10995  addassnq  10998  mulassnq  10999  distrnq  11001  mulidnq  11003  recmulnq  11004  ltsonq  11009  lterpq  11010  ltanq  11011  ltmnq  11012  ltexnq  11015  archnq  11020  elreal2  11172  cnref1o  13027  fsum2dlem  15806  fsumcom2  15810  ackbijnn  15864  fprod2dlem  16016  fprodcom2  16020  ruclem6  16271  ruclem8  16273  ruclem9  16274  ruclem10  16275  ruclem11  16276  ruclem12  16277  eucalgval  16619  eucalginv  16621  eucalglt  16622  eucalg  16624  xpsff1o  17612  comfffval2  17744  comfeq  17749  idfucl  17926  funcpropd  17947  fucpropd  18025  xpccatid  18233  1stfcl  18242  2ndfcl  18243  xpcpropd  18253  hofcl  18304  hofpropd  18312  yonedalem3  18325  lsmhash  19723  gsum2dlem2  19989  evlslem4  22100  mdetunilem9  22626  tx2cn  23618  txdis  23640  txlly  23644  txnlly  23645  txhaus  23655  txkgen  23660  txconn  23697  txhmeo  23811  ptuncnv  23815  ptunhmeo  23816  xkohmeo  23823  utop2nei  24259  utop3cls  24260  imasdsf1olem  24383  cnheiborlem  24986  caubl  25342  caublcls  25343  bcthlem2  25359  bcthlem4  25361  bcthlem5  25362  ovolficcss  25504  ovoliunlem1  25537  ovoliunlem2  25538  ovolicc2lem1  25552  ovolicc2lem2  25553  ovolicc2lem4  25555  ovolicc2lem5  25556  dyadmbl  25635  fsumvma  27257  lgsquadlem1  27424  lgsquadlem2  27425  opreu2reuALT  32496  disjxpin  32601  fsumiunle  32831  gsummpt2d  33052  gsumwrd2dccatlem  33069  elrgspnlem2  33247  elrgspnsubrunlem2  33252  erler  33269  rlocaddval  33272  rlocmulval  33273  cnre2csqima  33910  tpr2rico  33911  esum2dlem  34093  esumiun  34095  2ndmbfm  34263  sxbrsigalem0  34273  dya2iocnrect  34283  sibfof  34342  sitgaddlemb  34350  hgt750lemb  34671  satefvfmla0  35423  msubff  35535  msubco  35536  mpst123  35545  msubvrs  35565  funtransport  36032  filnetlem3  36381  elxp8  37372  finixpnum  37612  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  heicant  37662  mblfinlem1  37664  mblfinlem2  37665  ftc2nc  37709  heiborlem8  37825  dvhb1dimN  40988  dvhvaddcl  41097  dvhvaddcomN  41098  dvhvscacl  41105  dvhgrp  41109  dvhlveclem  41110  dibelval1st  41151  dicelval1stN  41190  aks6d1c2p1  42119  aks6d1c3  42124  aks6d1c4  42125  aks6d1c6lem2  42172  aks6d1c6lem4  42174  f1o2d2  42274  rmxypairf1o  42923  frmx  42925  cnmetcoval  45207  dvnprodlem1  45961  dvnprodlem2  45962  volicoff  46010  voliooicof  46011  etransclem44  46293  etransclem45  46294  etransclem47  46296  hoissre  46559  hoiprodcl  46562  ovnsubaddlem1  46585  ovnhoilem2  46617  hoicoto2  46620  ovncvr2  46626  opnvonmbllem2  46648  ovolval2lem  46658  ovolval3  46662  ovolval4lem1  46664  ovolval4lem2  46665  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  smfpimbor1lem1  46813  2arymaptf  48573  rrx2xpref1o  48639  elxpcbasex1ALT  48955  swapf2f1oa  48983  swapfida  48986  fuco2eld2  49009  fucoco2  49053  pgindlem  49234