Theorem xp1st 7723

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 5580	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3499	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3499	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7701	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2899	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 480	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 715	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1933	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 219	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ⟨cop 4575   × cxp 5555  ‘cfv 6357  1^st c1st 7689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-iota 6316  df-fun 6359  df-fv 6365  df-1st 7691

This theorem is referenced by:  el2xptp0  7738  offval22  7785  fimaproj  7831  xpf1o  8681  xpmapenlem  8686  mapunen  8688  unxpwdom2  9054  djulf1o  9343  djurf1o  9344  djur  9350  eldju1st  9354  r0weon  9440  infxpenlem  9441  fseqdom  9454  iundom2g  9964  enqbreq2  10344  nqereu  10353  addpqf  10368  mulpqf  10370  adderpqlem  10378  mulerpqlem  10379  addassnq  10382  mulassnq  10383  distrnq  10385  mulidnq  10387  recmulnq  10388  ltsonq  10393  lterpq  10394  ltanq  10395  ltmnq  10396  ltexnq  10399  archnq  10404  elreal2  10556  cnref1o  12387  fsum2dlem  15127  fsumcom2  15131  ackbijnn  15185  fprod2dlem  15336  fprodcom2  15340  ruclem6  15590  ruclem8  15592  ruclem9  15593  ruclem10  15594  ruclem11  15595  ruclem12  15596  eucalgval  15928  eucalginv  15930  eucalglt  15931  eucalg  15933  xpsff1o  16842  comfffval2  16973  comfeq  16978  idfucl  17153  funcpropd  17172  fucpropd  17249  xpccatid  17440  1stfcl  17449  2ndfcl  17450  xpcpropd  17460  hofcl  17511  hofpropd  17519  yonedalem3  17532  lsmhash  18833  gsum2dlem2  19093  evlslem4  20290  mdetunilem9  21231  tx2cn  22220  txdis  22242  txlly  22246  txnlly  22247  txhaus  22257  txkgen  22262  txconn  22299  txhmeo  22413  ptuncnv  22417  ptunhmeo  22418  xkohmeo  22425  utop2nei  22861  utop3cls  22862  imasdsf1olem  22985  cnheiborlem  23560  caubl  23913  caublcls  23914  bcthlem2  23930  bcthlem4  23932  bcthlem5  23933  ovolficcss  24072  ovoliunlem1  24105  ovoliunlem2  24106  ovolicc2lem1  24120  ovolicc2lem2  24121  ovolicc2lem4  24123  ovolicc2lem5  24124  dyadmbl  24203  fsumvma  25791  lgsquadlem1  25958  lgsquadlem2  25959  opreu2reuALT  30242  disjxpin  30340  fsumiunle  30547  gsummpt2d  30689  cnre2csqima  31156  tpr2rico  31157  esum2dlem  31353  esumiun  31355  2ndmbfm  31521  sxbrsigalem0  31531  dya2iocnrect  31541  sibfof  31600  sitgaddlemb  31608  hgt750lemb  31929  satefvfmla0  32667  msubff  32779  msubco  32780  mpst123  32789  msubvrs  32809  funtransport  33494  filnetlem3  33730  elxp8  34654  finixpnum  34879  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem9  34903  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem13  34907  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  poimirlem29  34923  poimirlem30  34924  poimirlem31  34925  poimirlem32  34926  heicant  34929  mblfinlem1  34931  mblfinlem2  34932  ftc2nc  34978  heiborlem8  35098  dvhb1dimN  38124  dvhvaddcl  38233  dvhvaddcomN  38234  dvhvscacl  38241  dvhgrp  38245  dvhlveclem  38246  dibelval1st  38287  dicelval1stN  38326  rmxypairf1o  39515  frmx  39517  cnmetcoval  41472  dvnprodlem1  42238  dvnprodlem2  42239  volicoff  42287  voliooicof  42288  etransclem44  42570  etransclem45  42571  etransclem47  42573  hoissre  42833  hoiprodcl  42836  ovnsubaddlem1  42859  ovnhoilem2  42891  hoicoto2  42894  ovncvr2  42900  opnvonmbllem2  42922  ovolval2lem  42932  ovolval3  42936  ovolval4lem1  42938  ovolval4lem2  42939  ovolval5lem2  42942  ovnovollem1  42945  ovnovollem2  42946  smfpimbor1lem1  43080  rrx2xpref1o  44712