Theorem xp1st 7970

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 5648	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3436	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3436	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7948	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2825	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 478	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 723	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1939	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 218	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ⟨cop 4568   × cxp 5623  ‘cfv 6492  1^st c1st 7936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fv 6500  df-1st 7938

This theorem is referenced by:  el2xptp0  7985  offval22  8034  mpof1o2d  8072  fimaproj  8082  xpf1o  9074  xpmapenlem  9079  mapunen  9081  unxpwdom2  9500  djulf1o  9834  djurf1o  9835  djur  9841  eldju1st  9845  r0weon  9932  infxpenlem  9933  fseqdom  9946  iundom2g  10460  enqbreq2  10841  nqereu  10850  addpqf  10865  mulpqf  10867  adderpqlem  10875  mulerpqlem  10876  addassnq  10879  mulassnq  10880  distrnq  10882  mulidnq  10884  recmulnq  10885  ltsonq  10890  lterpq  10891  ltanq  10892  ltmnq  10893  ltexnq  10896  archnq  10901  elreal2  11053  cnref1o  12933  fsum2dlem  15730  fsumcom2  15734  ackbijnn  15791  fprod2dlem  15943  fprodcom2  15947  ruclem6  16200  ruclem8  16202  ruclem9  16203  ruclem10  16204  ruclem11  16205  ruclem12  16206  eucalgval  16549  eucalginv  16551  eucalglt  16552  eucalg  16554  xpsff1o  17529  comfffval2  17665  comfeq  17670  idfucl  17846  funcpropd  17867  fucpropd  17945  xpccatid  18152  1stfcl  18161  2ndfcl  18162  xpcpropd  18172  hofcl  18223  hofpropd  18231  yonedalem3  18244  lsmhash  19678  gsum2dlem2  19944  evlslem4  22059  mdetunilem9  22610  tx2cn  23600  txdis  23622  txlly  23626  txnlly  23627  txhaus  23637  txkgen  23642  txconn  23679  txhmeo  23793  ptuncnv  23797  ptunhmeo  23798  xkohmeo  23805  utop2nei  24240  utop3cls  24241  imasdsf1olem  24363  cnheiborlem  24946  caubl  25300  caublcls  25301  bcthlem2  25317  bcthlem4  25319  bcthlem5  25320  ovolficcss  25461  ovoliunlem1  25494  ovoliunlem2  25495  ovolicc2lem1  25509  ovolicc2lem2  25510  ovolicc2lem4  25512  ovolicc2lem5  25513  dyadmbl  25592  fsumvma  27201  lgsquadlem1  27368  lgsquadlem2  27369  opreu2reuALT  32571  disjxpin  32684  fsumiunle  32928  gsummpt2d  33137  gsumwrd2dccatlem  33165  conjga  33258  elrgspnlem2  33331  elrgspnsubrunlem2  33336  erler  33353  rlocaddval  33356  rlocmulval  33357  mplvrpmga  33736  cnre2csqima  34102  tpr2rico  34103  esum2dlem  34283  esumiun  34285  2ndmbfm  34452  sxbrsigalem0  34462  dya2iocnrect  34472  sibfof  34531  sitgaddlemb  34539  hgt750lemb  34847  satefvfmla0  35647  msubff  35759  msubco  35760  mpst123  35769  msubvrs  35789  funtransport  36260  filnetlem3  36609  elxp8  37734  finixpnum  37973  poimirlem4  37992  poimirlem5  37993  poimirlem6  37994  poimirlem7  37995  poimirlem8  37996  poimirlem9  37997  poimirlem10  37998  poimirlem11  37999  poimirlem12  38000  poimirlem13  38001  poimirlem14  38002  poimirlem15  38003  poimirlem16  38004  poimirlem17  38005  poimirlem18  38006  poimirlem19  38007  poimirlem20  38008  poimirlem21  38009  poimirlem22  38010  poimirlem25  38013  poimirlem26  38014  poimirlem27  38015  poimirlem29  38017  poimirlem30  38018  poimirlem31  38019  poimirlem32  38020  heicant  38023  mblfinlem1  38025  mblfinlem2  38026  ftc2nc  38070  heiborlem8  38186  dvhb1dimN  41479  dvhvaddcl  41588  dvhvaddcomN  41589  dvhvscacl  41596  dvhgrp  41600  dvhlveclem  41601  dibelval1st  41642  dicelval1stN  41681  aks6d1c2p1  42604  aks6d1c3  42609  aks6d1c4  42610  aks6d1c6lem2  42657  aks6d1c6lem4  42659  rmxypairf1o  43357  frmx  43359  cnmetcoval  45649  dvnprodlem1  46390  dvnprodlem2  46391  volicoff  46439  voliooicof  46440  etransclem44  46722  etransclem45  46723  etransclem47  46725  hoissre  46988  hoiprodcl  46991  ovnsubaddlem1  47014  ovnhoilem2  47046  hoicoto2  47049  ovncvr2  47055  opnvonmbllem2  47077  ovolval2lem  47087  ovolval3  47091  ovolval4lem1  47093  ovolval4lem2  47094  ovolval5lem2  47097  ovnovollem1  47100  ovnovollem2  47101  smfpimbor1lem1  47242  2arymaptf  49144  rrx2xpref1o  49210  elxpcbasex1ALT  49740  swapf2f1oa  49768  swapfida  49771  fuco2eld2  49805  fucoco2  49849  pgindlem  50206