Theorem xp1st 8000

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 5689	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3470	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3470	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7978	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2810	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 714	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1927	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1533  ∃wex 1773   ∈ wcel 2098  ⟨cop 4626   × cxp 5664  ‘cfv 6533  1^st c1st 7966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6485  df-fun 6535  df-fv 6541  df-1st 7968

This theorem is referenced by:  el2xptp0  8015  offval22  8068  fimaproj  8115  xpf1o  9135  xpmapenlem  9140  mapunen  9142  unxpwdom2  9579  djulf1o  9903  djurf1o  9904  djur  9910  eldju1st  9914  r0weon  10003  infxpenlem  10004  fseqdom  10017  iundom2g  10531  enqbreq2  10911  nqereu  10920  addpqf  10935  mulpqf  10937  adderpqlem  10945  mulerpqlem  10946  addassnq  10949  mulassnq  10950  distrnq  10952  mulidnq  10954  recmulnq  10955  ltsonq  10960  lterpq  10961  ltanq  10962  ltmnq  10963  ltexnq  10966  archnq  10971  elreal2  11123  cnref1o  12966  fsum2dlem  15713  fsumcom2  15717  ackbijnn  15771  fprod2dlem  15921  fprodcom2  15925  ruclem6  16175  ruclem8  16177  ruclem9  16178  ruclem10  16179  ruclem11  16180  ruclem12  16181  eucalgval  16516  eucalginv  16518  eucalglt  16519  eucalg  16521  xpsff1o  17512  comfffval2  17644  comfeq  17649  idfucl  17830  funcpropd  17852  fucpropd  17932  xpccatid  18142  1stfcl  18151  2ndfcl  18152  xpcpropd  18163  hofcl  18214  hofpropd  18222  yonedalem3  18235  lsmhash  19615  gsum2dlem2  19881  evlslem4  21947  mdetunilem9  22444  tx2cn  23436  txdis  23458  txlly  23462  txnlly  23463  txhaus  23473  txkgen  23478  txconn  23515  txhmeo  23629  ptuncnv  23633  ptunhmeo  23634  xkohmeo  23641  utop2nei  24077  utop3cls  24078  imasdsf1olem  24201  cnheiborlem  24802  caubl  25158  caublcls  25159  bcthlem2  25175  bcthlem4  25177  bcthlem5  25178  ovolficcss  25320  ovoliunlem1  25353  ovoliunlem2  25354  ovolicc2lem1  25368  ovolicc2lem2  25369  ovolicc2lem4  25371  ovolicc2lem5  25372  dyadmbl  25451  fsumvma  27062  lgsquadlem1  27229  lgsquadlem2  27230  opreu2reuALT  32186  disjxpin  32288  fsumiunle  32502  gsummpt2d  32669  cnre2csqima  33380  tpr2rico  33381  esum2dlem  33579  esumiun  33581  2ndmbfm  33749  sxbrsigalem0  33759  dya2iocnrect  33769  sibfof  33828  sitgaddlemb  33836  hgt750lemb  34157  satefvfmla0  34898  msubff  35010  msubco  35011  mpst123  35020  msubvrs  35040  funtransport  35498  filnetlem3  35755  elxp8  36742  finixpnum  36963  poimirlem4  36982  poimirlem5  36983  poimirlem6  36984  poimirlem7  36985  poimirlem8  36986  poimirlem9  36987  poimirlem10  36988  poimirlem11  36989  poimirlem12  36990  poimirlem13  36991  poimirlem14  36992  poimirlem15  36993  poimirlem16  36994  poimirlem17  36995  poimirlem18  36996  poimirlem19  36997  poimirlem20  36998  poimirlem21  36999  poimirlem22  37000  poimirlem25  37003  poimirlem26  37004  poimirlem27  37005  poimirlem29  37007  poimirlem30  37008  poimirlem31  37009  poimirlem32  37010  heicant  37013  mblfinlem1  37015  mblfinlem2  37016  ftc2nc  37060  heiborlem8  37176  dvhb1dimN  40347  dvhvaddcl  40456  dvhvaddcomN  40457  dvhvscacl  40464  dvhgrp  40468  dvhlveclem  40469  dibelval1st  40510  dicelval1stN  40549  aks6d1c2p1  41449  f1o2d2  41548  rmxypairf1o  42139  frmx  42141  cnmetcoval  44386  dvnprodlem1  45147  dvnprodlem2  45148  volicoff  45196  voliooicof  45197  etransclem44  45479  etransclem45  45480  etransclem47  45482  hoissre  45745  hoiprodcl  45748  ovnsubaddlem1  45771  ovnhoilem2  45803  hoicoto2  45806  ovncvr2  45812  opnvonmbllem2  45834  ovolval2lem  45844  ovolval3  45848  ovolval4lem1  45850  ovolval4lem2  45851  ovolval5lem2  45854  ovnovollem1  45857  ovnovollem2  45858  smfpimbor1lem1  45999  2arymaptf  47526  rrx2xpref1o  47592  pgindlem  47948