Theorem xp1st 8016

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 5670	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3454	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3454	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7994	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2845	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 483	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 730	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1965	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ⟨cop 4589   × cxp 5645  ‘cfv 6527  1^st c1st 7982

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-iota 6483  df-fun 6529  df-fv 6535  df-1st 7984

This theorem is used by:  el2xptp0  8030  offval22  8082  mpof1o2d  8120  fimaproj  8130  xpf1o  9136  xpmapenlem  9141  mapunen  9143  unxpwdom2  9560  djulf1o  9965  djurf1o  9966  djur  9972  eldju1st  9976  r0weon  10063  infxpenlem  10064  fseqdom  10077  iundom2g  10596  enqbreq2  10977  nqereu  10986  addpqf  11001  mulpqf  11003  adderpqlem  11011  mulerpqlem  11012  addassnq  11015  mulassnq  11016  distrnq  11018  mulidnq  11020  recmulnq  11021  ltsonq  11026  lterpq  11027  ltanq  11028  ltmnq  11029  ltexnq  11032  archnq  11037  elreal2  11189  cnref1o  13083  fsum2dlem  15904  fsumcom2  15908  ackbijnn  15965  fprod2dlem  16115  fprodcom2  16119  ruclem6  16371  ruclem8  16373  ruclem9  16374  ruclem10  16375  ruclem11  16376  ruclem12  16377  eucalgval  16720  eucalginv  16722  eucalglt  16723  eucalg  16725  xpsff1o  17701  comfffval2  17837  comfeq  17842  idfucl  18018  funcpropd  18039  fucpropd  18117  xpccatid  18324  1stfcl  18333  2ndfcl  18334  xpcpropd  18344  hofcl  18395  hofpropd  18403  yonedalem3  18416  lsmhash  19881  gsum2dlem2  20147  evlslem4  22347  mdetunilem9  22897  tx2cn  23891  txdis  23913  txlly  23917  txnlly  23918  txhaus  23928  txkgen  23933  txconn  23970  txhmeo  24084  ptuncnv  24088  ptunhmeo  24089  xkohmeo  24096  utop2nei  24531  utop3cls  24532  imasdsf1olem  24654  cnheiborlem  25237  caubl  25591  caublcls  25592  bcthlem2  25608  bcthlem4  25610  bcthlem5  25611  ovolficcss  25752  ovoliunlem1  25785  ovoliunlem2  25786  ovolicc2lem1  25800  ovolicc2lem2  25801  ovolicc2lem4  25803  ovolicc2lem5  25804  dyadmbl  25883  fsumvma  27504  lgsquadlem1  27671  lgsquadlem2  27672  opreu2reuALT  33007  disjxpin  33116  fsumiunle  33354  gsummpt2d  33544  gsumwrd2dccatlem  33572  conjga  33665  elrgspnlem2  33738  elrgspnsubrunlem2  33743  erler  33760  rlocaddval  33764  rlocmulval  33765  mplvrpmga  34111  cnre2csqima  34477  tpr2rico  34478  esum2dlem  34658  esumiun  34660  2ndmbfm  34828  sxbrsigalem0  34838  dya2iocnrect  34848  sibfof  34907  sitgaddlemb  34915  hgt750lemb  35220  satefvfmla0  36104  msubff  36216  msubco  36217  mpst123  36226  msubvrs  36246  funtransport  36718  filnetlem3  37090  elxp8  38214  finixpnum  38448  poimirlem4  38462  poimirlem5  38463  poimirlem6  38464  poimirlem7  38465  poimirlem8  38466  poimirlem9  38467  poimirlem10  38468  poimirlem11  38469  poimirlem12  38470  poimirlem13  38471  poimirlem14  38472  poimirlem15  38473  poimirlem16  38474  poimirlem17  38475  poimirlem18  38476  poimirlem19  38477  poimirlem20  38478  poimirlem21  38479  poimirlem22  38480  poimirlem25  38483  poimirlem26  38484  poimirlem27  38485  poimirlem29  38487  poimirlem30  38488  poimirlem31  38489  poimirlem32  38490  heicant  38493  mblfinlem1  38495  mblfinlem2  38496  ftc2nc  38540  heiborlem8  38672  dvhb1dimN  41963  dvhvaddcl  42072  dvhvaddcomN  42073  dvhvscacl  42080  dvhgrp  42084  dvhlveclem  42085  dibelval1st  42126  dicelval1stN  42165  aks6d1c2p1  43088  aks6d1c3  43093  aks6d1c4  43094  aks6d1c6lem2  43141  aks6d1c6lem4  43143  rmxypairf1o  43856  frmx  43858  cnmetcoval  46137  dvnprodlem1  46878  dvnprodlem2  46879  volicoff  46927  voliooicof  46928  etransclem44  47210  etransclem45  47211  etransclem47  47213  hoissre  47476  hoiprodcl  47479  ovnsubaddlem1  47502  ovnhoilem2  47534  hoicoto2  47537  ovncvr2  47543  opnvonmbllem2  47565  ovolval2lem  47575  ovolval3  47579  ovolval4lem1  47581  ovolval4lem2  47582  ovolval5lem2  47585  ovnovollem1  47588  ovnovollem2  47589  smfpimbor1lem1  47730  2arymaptf  49686  rrx2xpref1o  49752  elxpcbasex1ALT  50279  swapf2f1oa  50307  swapfida  50310  fuco2eld2  50344  fucoco2  50388  pgindlem  50730