Theorem xp1st 8028

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ⟨cop 4612   × cxp 5663  ‘cfv 6541  1^st c1st 7994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-iota 6494  df-fun 6543  df-fv 6549  df-1st 7996

This theorem is referenced by:  el2xptp0  8043  offval22  8095  fimaproj  8142  xpf1o  9161  xpmapenlem  9166  mapunen  9168  unxpwdom2  9610  djulf1o  9934  djurf1o  9935  djur  9941  eldju1st  9945  r0weon  10034  infxpenlem  10035  fseqdom  10048  iundom2g  10562  enqbreq2  10942  nqereu  10951  addpqf  10966  mulpqf  10968  adderpqlem  10976  mulerpqlem  10977  addassnq  10980  mulassnq  10981  distrnq  10983  mulidnq  10985  recmulnq  10986  ltsonq  10991  lterpq  10992  ltanq  10993  ltmnq  10994  ltexnq  10997  archnq  11002  elreal2  11154  cnref1o  13009  fsum2dlem  15789  fsumcom2  15793  ackbijnn  15847  fprod2dlem  15999  fprodcom2  16003  ruclem6  16254  ruclem8  16256  ruclem9  16257  ruclem10  16258  ruclem11  16259  ruclem12  16260  eucalgval  16602  eucalginv  16604  eucalglt  16605  eucalg  16607  xpsff1o  17584  comfffval2  17716  comfeq  17721  idfucl  17898  funcpropd  17919  fucpropd  17997  xpccatid  18204  1stfcl  18213  2ndfcl  18214  xpcpropd  18224  hofcl  18275  hofpropd  18283  yonedalem3  18296  lsmhash  19692  gsum2dlem2  19958  evlslem4  22049  mdetunilem9  22575  tx2cn  23565  txdis  23587  txlly  23591  txnlly  23592  txhaus  23602  txkgen  23607  txconn  23644  txhmeo  23758  ptuncnv  23762  ptunhmeo  23763  xkohmeo  23770  utop2nei  24206  utop3cls  24207  imasdsf1olem  24329  cnheiborlem  24923  caubl  25279  caublcls  25280  bcthlem2  25296  bcthlem4  25298  bcthlem5  25299  ovolficcss  25441  ovoliunlem1  25474  ovoliunlem2  25475  ovolicc2lem1  25489  ovolicc2lem2  25490  ovolicc2lem4  25492  ovolicc2lem5  25493  dyadmbl  25572  fsumvma  27194  lgsquadlem1  27361  lgsquadlem2  27362  opreu2reuALT  32425  disjxpin  32537  fsumiunle  32776  gsummpt2d  32996  gsumwrd2dccatlem  33013  elrgspnlem2  33191  elrgspnsubrunlem2  33196  erler  33213  rlocaddval  33216  rlocmulval  33217  cnre2csqima  33885  tpr2rico  33886  esum2dlem  34068  esumiun  34070  2ndmbfm  34238  sxbrsigalem0  34248  dya2iocnrect  34258  sibfof  34317  sitgaddlemb  34325  hgt750lemb  34646  satefvfmla0  35398  msubff  35510  msubco  35511  mpst123  35520  msubvrs  35540  funtransport  36007  filnetlem3  36356  elxp8  37347  finixpnum  37587  poimirlem4  37606  poimirlem5  37607  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem9  37611  poimirlem10  37612  poimirlem11  37613  poimirlem12  37614  poimirlem13  37615  poimirlem14  37616  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem18  37620  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem25  37627  poimirlem26  37628  poimirlem27  37629  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  poimirlem32  37634  heicant  37637  mblfinlem1  37639  mblfinlem2  37640  ftc2nc  37684  heiborlem8  37800  dvhb1dimN  40963  dvhvaddcl  41072  dvhvaddcomN  41073  dvhvscacl  41080  dvhgrp  41084  dvhlveclem  41085  dibelval1st  41126  dicelval1stN  41165  aks6d1c2p1  42094  aks6d1c3  42099  aks6d1c4  42100  aks6d1c6lem2  42147  aks6d1c6lem4  42149  f1o2d2  42248  rmxypairf1o  42901  frmx  42903  cnmetcoval  45179  dvnprodlem1  45933  dvnprodlem2  45934  volicoff  45982  voliooicof  45983  etransclem44  46265  etransclem45  46266  etransclem47  46268  hoissre  46531  hoiprodcl  46534  ovnsubaddlem1  46557  ovnhoilem2  46589  hoicoto2  46592  ovncvr2  46598  opnvonmbllem2  46620  ovolval2lem  46630  ovolval3  46634  ovolval4lem1  46636  ovolval4lem2  46637  ovolval5lem2  46640  ovnovollem1  46643  ovnovollem2  46644  smfpimbor1lem1  46785  2arymaptf  48546  rrx2xpref1o  48612  elxpcbasex1ALT  49000  swapf2f1oa  49028  swapfida  49031  fuco2eld2  49059  fucoco2  49103  pgindlem  49329