Theorem xp1st 8021

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 5682	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3457	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3457	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7999	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2847	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 483	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 730	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1965	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ⟨cop 4593   × cxp 5657  ‘cfv 6537  1^st c1st 7987

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fv 6545  df-1st 7989

This theorem is used by:  el2xptp0  8036  offval22  8088  mpof1o2d  8126  fimaproj  8136  xpf1o  9140  xpmapenlem  9145  mapunen  9147  unxpwdom2  9563  djulf1o  9920  djurf1o  9921  djur  9927  eldju1st  9931  r0weon  10018  infxpenlem  10019  fseqdom  10032  iundom2g  10551  enqbreq2  10932  nqereu  10941  addpqf  10956  mulpqf  10958  adderpqlem  10966  mulerpqlem  10967  addassnq  10970  mulassnq  10971  distrnq  10973  mulidnq  10975  recmulnq  10976  ltsonq  10981  lterpq  10982  ltanq  10983  ltmnq  10984  ltexnq  10987  archnq  10992  elreal2  11144  cnref1o  13037  fsum2dlem  15858  fsumcom2  15862  ackbijnn  15919  fprod2dlem  16071  fprodcom2  16075  ruclem6  16327  ruclem8  16329  ruclem9  16330  ruclem10  16331  ruclem11  16332  ruclem12  16333  eucalgval  16676  eucalginv  16678  eucalglt  16679  eucalg  16681  xpsff1o  17657  comfffval2  17793  comfeq  17798  idfucl  17974  funcpropd  17995  fucpropd  18073  xpccatid  18280  1stfcl  18289  2ndfcl  18290  xpcpropd  18300  hofcl  18351  hofpropd  18359  yonedalem3  18372  lsmhash  19836  gsum2dlem2  20102  evlslem4  22296  mdetunilem9  22846  tx2cn  23840  txdis  23862  txlly  23866  txnlly  23867  txhaus  23877  txkgen  23882  txconn  23919  txhmeo  24033  ptuncnv  24037  ptunhmeo  24038  xkohmeo  24045  utop2nei  24480  utop3cls  24481  imasdsf1olem  24603  cnheiborlem  25186  caubl  25540  caublcls  25541  bcthlem2  25557  bcthlem4  25559  bcthlem5  25560  ovolficcss  25701  ovoliunlem1  25734  ovoliunlem2  25735  ovolicc2lem1  25749  ovolicc2lem2  25750  ovolicc2lem4  25752  ovolicc2lem5  25753  dyadmbl  25832  fsumvma  27450  lgsquadlem1  27617  lgsquadlem2  27618  opreu2reuALT  32953  disjxpin  33063  fsumiunle  33301  gsummpt2d  33491  gsumwrd2dccatlem  33519  conjga  33612  elrgspnlem2  33685  elrgspnsubrunlem2  33690  erler  33707  rlocaddval  33711  rlocmulval  33712  mplvrpmga  34057  cnre2csqima  34423  tpr2rico  34424  esum2dlem  34604  esumiun  34606  2ndmbfm  34774  sxbrsigalem0  34784  dya2iocnrect  34794  sibfof  34853  sitgaddlemb  34861  hgt750lemb  35166  satefvfmla0  35999  msubff  36111  msubco  36112  mpst123  36121  msubvrs  36141  funtransport  36613  filnetlem3  37001  elxp8  38127  finixpnum  38361  poimirlem4  38375  poimirlem5  38376  poimirlem6  38377  poimirlem7  38378  poimirlem8  38379  poimirlem9  38380  poimirlem10  38381  poimirlem11  38382  poimirlem12  38383  poimirlem13  38384  poimirlem14  38385  poimirlem15  38386  poimirlem16  38387  poimirlem17  38388  poimirlem18  38389  poimirlem19  38390  poimirlem20  38391  poimirlem21  38392  poimirlem22  38393  poimirlem25  38396  poimirlem26  38397  poimirlem27  38398  poimirlem29  38400  poimirlem30  38401  poimirlem31  38402  poimirlem32  38403  heicant  38406  mblfinlem1  38408  mblfinlem2  38409  ftc2nc  38453  heiborlem8  38570  dvhb1dimN  41861  dvhvaddcl  41970  dvhvaddcomN  41971  dvhvscacl  41978  dvhgrp  41982  dvhlveclem  41983  dibelval1st  42024  dicelval1stN  42063  aks6d1c2p1  42986  aks6d1c3  42991  aks6d1c4  42992  aks6d1c6lem2  43039  aks6d1c6lem4  43041  rmxypairf1o  43754  frmx  43756  cnmetcoval  46035  dvnprodlem1  46776  dvnprodlem2  46777  volicoff  46825  voliooicof  46826  etransclem44  47108  etransclem45  47109  etransclem47  47111  hoissre  47374  hoiprodcl  47377  ovnsubaddlem1  47400  ovnhoilem2  47432  hoicoto2  47435  ovncvr2  47441  opnvonmbllem2  47463  ovolval2lem  47473  ovolval3  47477  ovolval4lem1  47479  ovolval4lem2  47480  ovolval5lem2  47483  ovnovollem1  47486  ovnovollem2  47487  smfpimbor1lem1  47628  2arymaptf  49584  rrx2xpref1o  49650  elxpcbasex1ALT  50177  swapf2f1oa  50205  swapfida  50208  fuco2eld2  50242  fucoco2  50286  pgindlem  50643