Theorem xp1st 7895

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 5623	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3441	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3441	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7873	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2821	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 479	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 715	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1933	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539  ∃wex 1779   ∈ wcel 2104  ⟨cop 4571   × cxp 5598  ‘cfv 6458  1^st c1st 7861

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-iota 6410  df-fun 6460  df-fv 6466  df-1st 7863

This theorem is referenced by:  el2xptp0  7910  offval22  7960  fimaproj  8007  xpf1o  8964  xpmapenlem  8969  mapunen  8971  unxpwdom2  9391  djulf1o  9714  djurf1o  9715  djur  9721  eldju1st  9725  r0weon  9814  infxpenlem  9815  fseqdom  9828  iundom2g  10342  enqbreq2  10722  nqereu  10731  addpqf  10746  mulpqf  10748  adderpqlem  10756  mulerpqlem  10757  addassnq  10760  mulassnq  10761  distrnq  10763  mulidnq  10765  recmulnq  10766  ltsonq  10771  lterpq  10772  ltanq  10773  ltmnq  10774  ltexnq  10777  archnq  10782  elreal2  10934  cnref1o  12771  fsum2dlem  15527  fsumcom2  15531  ackbijnn  15585  fprod2dlem  15735  fprodcom2  15739  ruclem6  15989  ruclem8  15991  ruclem9  15992  ruclem10  15993  ruclem11  15994  ruclem12  15995  eucalgval  16332  eucalginv  16334  eucalglt  16335  eucalg  16337  xpsff1o  17323  comfffval2  17455  comfeq  17460  idfucl  17641  funcpropd  17661  fucpropd  17740  xpccatid  17950  1stfcl  17959  2ndfcl  17960  xpcpropd  17971  hofcl  18022  hofpropd  18030  yonedalem3  18043  lsmhash  19356  gsum2dlem2  19617  evlslem4  21329  mdetunilem9  21814  tx2cn  22806  txdis  22828  txlly  22832  txnlly  22833  txhaus  22843  txkgen  22848  txconn  22885  txhmeo  22999  ptuncnv  23003  ptunhmeo  23004  xkohmeo  23011  utop2nei  23447  utop3cls  23448  imasdsf1olem  23571  cnheiborlem  24162  caubl  24517  caublcls  24518  bcthlem2  24534  bcthlem4  24536  bcthlem5  24537  ovolficcss  24678  ovoliunlem1  24711  ovoliunlem2  24712  ovolicc2lem1  24726  ovolicc2lem2  24727  ovolicc2lem4  24729  ovolicc2lem5  24730  dyadmbl  24809  fsumvma  26406  lgsquadlem1  26573  lgsquadlem2  26574  opreu2reuALT  30870  disjxpin  30972  fsumiunle  31188  gsummpt2d  31354  cnre2csqima  31906  tpr2rico  31907  esum2dlem  32105  esumiun  32107  2ndmbfm  32273  sxbrsigalem0  32283  dya2iocnrect  32293  sibfof  32352  sitgaddlemb  32360  hgt750lemb  32681  satefvfmla0  33425  msubff  33537  msubco  33538  mpst123  33547  msubvrs  33567  funtransport  34378  filnetlem3  34614  elxp8  35586  finixpnum  35806  poimirlem4  35825  poimirlem5  35826  poimirlem6  35827  poimirlem7  35828  poimirlem8  35829  poimirlem9  35830  poimirlem10  35831  poimirlem11  35832  poimirlem12  35833  poimirlem13  35834  poimirlem14  35835  poimirlem15  35836  poimirlem16  35837  poimirlem17  35838  poimirlem18  35839  poimirlem19  35840  poimirlem20  35841  poimirlem21  35842  poimirlem22  35843  poimirlem25  35846  poimirlem26  35847  poimirlem27  35848  poimirlem29  35850  poimirlem30  35851  poimirlem31  35852  poimirlem32  35853  heicant  35856  mblfinlem1  35858  mblfinlem2  35859  ftc2nc  35903  heiborlem8  36020  dvhb1dimN  39042  dvhvaddcl  39151  dvhvaddcomN  39152  dvhvscacl  39159  dvhgrp  39163  dvhlveclem  39164  dibelval1st  39205  dicelval1stN  39244  rmxypairf1o  40771  frmx  40773  cnmetcoval  42786  dvnprodlem1  43536  dvnprodlem2  43537  volicoff  43585  voliooicof  43586  etransclem44  43868  etransclem45  43869  etransclem47  43871  hoissre  44132  hoiprodcl  44135  ovnsubaddlem1  44158  ovnhoilem2  44190  hoicoto2  44193  ovncvr2  44199  opnvonmbllem2  44221  ovolval2lem  44231  ovolval3  44235  ovolval4lem1  44237  ovolval4lem2  44238  ovolval5lem2  44241  ovnovollem1  44244  ovnovollem2  44245  smfpimbor1lem1  44386  2arymaptf  46056  rrx2xpref1o  46122