Theorem xp1st 8019

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 5695	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3473	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3473	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7997	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2813	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 716	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1928	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534  ∃wex 1774   ∈ wcel 2099  ⟨cop 4630   × cxp 5670  ‘cfv 6542  1^st c1st 7985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-iota 6494  df-fun 6544  df-fv 6550  df-1st 7987

This theorem is referenced by:  el2xptp0  8034  offval22  8087  fimaproj  8134  xpf1o  9155  xpmapenlem  9160  mapunen  9162  unxpwdom2  9603  djulf1o  9927  djurf1o  9928  djur  9934  eldju1st  9938  r0weon  10027  infxpenlem  10028  fseqdom  10041  iundom2g  10555  enqbreq2  10935  nqereu  10944  addpqf  10959  mulpqf  10961  adderpqlem  10969  mulerpqlem  10970  addassnq  10973  mulassnq  10974  distrnq  10976  mulidnq  10978  recmulnq  10979  ltsonq  10984  lterpq  10985  ltanq  10986  ltmnq  10987  ltexnq  10990  archnq  10995  elreal2  11147  cnref1o  12991  fsum2dlem  15740  fsumcom2  15744  ackbijnn  15798  fprod2dlem  15948  fprodcom2  15952  ruclem6  16203  ruclem8  16205  ruclem9  16206  ruclem10  16207  ruclem11  16208  ruclem12  16209  eucalgval  16544  eucalginv  16546  eucalglt  16547  eucalg  16549  xpsff1o  17540  comfffval2  17672  comfeq  17677  idfucl  17858  funcpropd  17880  fucpropd  17960  xpccatid  18170  1stfcl  18179  2ndfcl  18180  xpcpropd  18191  hofcl  18242  hofpropd  18250  yonedalem3  18263  lsmhash  19651  gsum2dlem2  19917  evlslem4  22007  mdetunilem9  22509  tx2cn  23501  txdis  23523  txlly  23527  txnlly  23528  txhaus  23538  txkgen  23543  txconn  23580  txhmeo  23694  ptuncnv  23698  ptunhmeo  23699  xkohmeo  23706  utop2nei  24142  utop3cls  24143  imasdsf1olem  24266  cnheiborlem  24867  caubl  25223  caublcls  25224  bcthlem2  25240  bcthlem4  25242  bcthlem5  25243  ovolficcss  25385  ovoliunlem1  25418  ovoliunlem2  25419  ovolicc2lem1  25433  ovolicc2lem2  25434  ovolicc2lem4  25436  ovolicc2lem5  25437  dyadmbl  25516  fsumvma  27133  lgsquadlem1  27300  lgsquadlem2  27301  opreu2reuALT  32261  disjxpin  32363  fsumiunle  32574  gsummpt2d  32741  cnre2csqima  33448  tpr2rico  33449  esum2dlem  33647  esumiun  33649  2ndmbfm  33817  sxbrsigalem0  33827  dya2iocnrect  33837  sibfof  33896  sitgaddlemb  33904  hgt750lemb  34224  satefvfmla0  34964  msubff  35076  msubco  35077  mpst123  35086  msubvrs  35106  funtransport  35563  filnetlem3  35800  elxp8  36786  finixpnum  37013  poimirlem4  37032  poimirlem5  37033  poimirlem6  37034  poimirlem7  37035  poimirlem8  37036  poimirlem9  37037  poimirlem10  37038  poimirlem11  37039  poimirlem12  37040  poimirlem13  37041  poimirlem14  37042  poimirlem15  37043  poimirlem16  37044  poimirlem17  37045  poimirlem18  37046  poimirlem19  37047  poimirlem20  37048  poimirlem21  37049  poimirlem22  37050  poimirlem25  37053  poimirlem26  37054  poimirlem27  37055  poimirlem29  37057  poimirlem30  37058  poimirlem31  37059  poimirlem32  37060  heicant  37063  mblfinlem1  37065  mblfinlem2  37066  ftc2nc  37110  heiborlem8  37226  dvhb1dimN  40396  dvhvaddcl  40505  dvhvaddcomN  40506  dvhvscacl  40513  dvhgrp  40517  dvhlveclem  40518  dibelval1st  40559  dicelval1stN  40598  aks6d1c2p1  41522  aks6d1c3  41527  aks6d1c6lem2  41575  f1o2d2  41644  rmxypairf1o  42254  frmx  42256  cnmetcoval  44498  dvnprodlem1  45257  dvnprodlem2  45258  volicoff  45306  voliooicof  45307  etransclem44  45589  etransclem45  45590  etransclem47  45592  hoissre  45855  hoiprodcl  45858  ovnsubaddlem1  45881  ovnhoilem2  45913  hoicoto2  45916  ovncvr2  45922  opnvonmbllem2  45944  ovolval2lem  45954  ovolval3  45958  ovolval4lem1  45960  ovolval4lem2  45961  ovolval5lem2  45964  ovnovollem1  45967  ovnovollem2  45968  smfpimbor1lem1  46109  2arymaptf  47648  rrx2xpref1o  47714  pgindlem  48069