Theorem xp1st 8017

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 5684	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3457	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3457	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7995	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2846	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 482	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 729	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1960	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568  ∃wex 1807   ∈ wcel 2141  ⟨cop 4594   × cxp 5659  ‘cfv 6536  1^st c1st 7983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fv 6544  df-1st 7985

This theorem is referenced by:  el2xptp0  8032  offval22  8082  mpof1o2d  8120  fimaproj  8130  xpf1o  9126  xpmapenlem  9131  mapunen  9133  unxpwdom2  9549  djulf1o  9897  djurf1o  9898  djur  9904  eldju1st  9908  r0weon  9995  infxpenlem  9996  fseqdom  10009  iundom2g  10523  enqbreq2  10904  nqereu  10913  addpqf  10928  mulpqf  10930  adderpqlem  10938  mulerpqlem  10939  addassnq  10942  mulassnq  10943  distrnq  10945  mulidnq  10947  recmulnq  10948  ltsonq  10953  lterpq  10954  ltanq  10955  ltmnq  10956  ltexnq  10959  archnq  10964  elreal2  11116  cnref1o  13008  fsum2dlem  15821  fsumcom2  15825  ackbijnn  15882  fprod2dlem  16034  fprodcom2  16038  ruclem6  16290  ruclem8  16292  ruclem9  16293  ruclem10  16294  ruclem11  16295  ruclem12  16296  eucalgval  16639  eucalginv  16641  eucalglt  16642  eucalg  16644  xpsff1o  17620  comfffval2  17756  comfeq  17761  idfucl  17937  funcpropd  17958  fucpropd  18036  xpccatid  18243  1stfcl  18252  2ndfcl  18253  xpcpropd  18263  hofcl  18314  hofpropd  18322  yonedalem3  18335  lsmhash  19774  gsum2dlem2  20040  evlslem4  22206  mdetunilem9  22756  tx2cn  23746  txdis  23768  txlly  23772  txnlly  23773  txhaus  23783  txkgen  23788  txconn  23825  txhmeo  23939  ptuncnv  23943  ptunhmeo  23944  xkohmeo  23951  utop2nei  24386  utop3cls  24387  imasdsf1olem  24509  cnheiborlem  25092  caubl  25446  caublcls  25447  bcthlem2  25463  bcthlem4  25465  bcthlem5  25466  ovolficcss  25607  ovoliunlem1  25640  ovoliunlem2  25641  ovolicc2lem1  25655  ovolicc2lem2  25656  ovolicc2lem4  25658  ovolicc2lem5  25659  dyadmbl  25738  fsumvma  27353  lgsquadlem1  27520  lgsquadlem2  27521  opreu2reuALT  32789  disjxpin  32899  fsumiunle  33139  gsummpt2d  33335  gsumwrd2dccatlem  33363  conjga  33456  elrgspnlem2  33529  elrgspnsubrunlem2  33534  erler  33551  rlocaddval  33555  rlocmulval  33556  mplvrpmga  33901  cnre2csqima  34267  tpr2rico  34268  esum2dlem  34448  esumiun  34450  2ndmbfm  34617  sxbrsigalem0  34627  dya2iocnrect  34637  sibfof  34696  sitgaddlemb  34704  hgt750lemb  35009  satefvfmla0  35876  msubff  35988  msubco  35989  mpst123  35998  msubvrs  36018  funtransport  36489  filnetlem3  36857  elxp8  37983  finixpnum  38222  poimirlem4  38241  poimirlem5  38242  poimirlem6  38243  poimirlem7  38244  poimirlem8  38245  poimirlem9  38246  poimirlem10  38247  poimirlem11  38248  poimirlem12  38249  poimirlem13  38250  poimirlem14  38251  poimirlem15  38252  poimirlem16  38253  poimirlem17  38254  poimirlem18  38255  poimirlem19  38256  poimirlem20  38257  poimirlem21  38258  poimirlem22  38259  poimirlem25  38262  poimirlem26  38263  poimirlem27  38264  poimirlem29  38266  poimirlem30  38267  poimirlem31  38268  poimirlem32  38269  heicant  38272  mblfinlem1  38274  mblfinlem2  38275  ftc2nc  38319  heiborlem8  38435  dvhb1dimN  41728  dvhvaddcl  41837  dvhvaddcomN  41838  dvhvscacl  41845  dvhgrp  41849  dvhlveclem  41850  dibelval1st  41891  dicelval1stN  41930  aks6d1c2p1  42853  aks6d1c3  42858  aks6d1c4  42859  aks6d1c6lem2  42906  aks6d1c6lem4  42908  rmxypairf1o  43608  frmx  43610  cnmetcoval  45889  dvnprodlem1  46630  dvnprodlem2  46631  volicoff  46679  voliooicof  46680  etransclem44  46962  etransclem45  46963  etransclem47  46965  hoissre  47228  hoiprodcl  47231  ovnsubaddlem1  47254  ovnhoilem2  47286  hoicoto2  47289  ovncvr2  47295  opnvonmbllem2  47317  ovolval2lem  47327  ovolval3  47331  ovolval4lem1  47333  ovolval4lem2  47334  ovolval5lem2  47337  ovnovollem1  47340  ovnovollem2  47341  smfpimbor1lem1  47482  2arymaptf  49399  rrx2xpref1o  49465  elxpcbasex1ALT  49994  swapf2f1oa  50022  swapfida  50025  fuco2eld2  50059  fucoco2  50103  pgindlem  50460