Theorem xp1st 7974

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 5654	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3434	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3434	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7952	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2822	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 718	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1934	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 217	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ⟨cop 4574   × cxp 5629  ‘cfv 6499  1^st c1st 7940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5376  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6455  df-fun 6501  df-fv 6507  df-1st 7942

This theorem is referenced by:  el2xptp0  7989  offval22  8038  fimaproj  8085  xpf1o  9077  xpmapenlem  9082  mapunen  9084  unxpwdom2  9503  djulf1o  9836  djurf1o  9837  djur  9843  eldju1st  9847  r0weon  9934  infxpenlem  9935  fseqdom  9948  iundom2g  10462  enqbreq2  10843  nqereu  10852  addpqf  10867  mulpqf  10869  adderpqlem  10877  mulerpqlem  10878  addassnq  10881  mulassnq  10882  distrnq  10884  mulidnq  10886  recmulnq  10887  ltsonq  10892  lterpq  10893  ltanq  10894  ltmnq  10895  ltexnq  10898  archnq  10903  elreal2  11055  cnref1o  12935  fsum2dlem  15732  fsumcom2  15736  ackbijnn  15793  fprod2dlem  15945  fprodcom2  15949  ruclem6  16202  ruclem8  16204  ruclem9  16205  ruclem10  16206  ruclem11  16207  ruclem12  16208  eucalgval  16551  eucalginv  16553  eucalglt  16554  eucalg  16556  xpsff1o  17531  comfffval2  17667  comfeq  17672  idfucl  17848  funcpropd  17869  fucpropd  17947  xpccatid  18154  1stfcl  18163  2ndfcl  18164  xpcpropd  18174  hofcl  18225  hofpropd  18233  yonedalem3  18246  lsmhash  19680  gsum2dlem2  19946  evlslem4  22054  mdetunilem9  22585  tx2cn  23575  txdis  23597  txlly  23601  txnlly  23602  txhaus  23612  txkgen  23617  txconn  23654  txhmeo  23768  ptuncnv  23772  ptunhmeo  23773  xkohmeo  23780  utop2nei  24215  utop3cls  24216  imasdsf1olem  24338  cnheiborlem  24921  caubl  25275  caublcls  25276  bcthlem2  25292  bcthlem4  25294  bcthlem5  25295  ovolficcss  25436  ovoliunlem1  25469  ovoliunlem2  25470  ovolicc2lem1  25484  ovolicc2lem2  25485  ovolicc2lem4  25487  ovolicc2lem5  25488  dyadmbl  25567  fsumvma  27176  lgsquadlem1  27343  lgsquadlem2  27344  opreu2reuALT  32546  disjxpin  32658  fsumiunle  32902  gsummpt2d  33110  gsumwrd2dccatlem  33138  conjga  33231  elrgspnlem2  33304  elrgspnsubrunlem2  33309  erler  33326  rlocaddval  33329  rlocmulval  33330  mplvrpmga  33689  cnre2csqima  34055  tpr2rico  34056  esum2dlem  34236  esumiun  34238  2ndmbfm  34405  sxbrsigalem0  34415  dya2iocnrect  34425  sibfof  34484  sitgaddlemb  34492  hgt750lemb  34800  satefvfmla0  35600  msubff  35712  msubco  35713  mpst123  35722  msubvrs  35742  funtransport  36213  filnetlem3  36562  elxp8  37687  finixpnum  37926  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  heicant  37976  mblfinlem1  37978  mblfinlem2  37979  ftc2nc  38023  heiborlem8  38139  dvhb1dimN  41432  dvhvaddcl  41541  dvhvaddcomN  41542  dvhvscacl  41549  dvhgrp  41553  dvhlveclem  41554  dibelval1st  41595  dicelval1stN  41634  aks6d1c2p1  42557  aks6d1c3  42562  aks6d1c4  42563  aks6d1c6lem2  42610  aks6d1c6lem4  42612  f1o2d2  42674  rmxypairf1o  43339  frmx  43341  cnmetcoval  45631  dvnprodlem1  46374  dvnprodlem2  46375  volicoff  46423  voliooicof  46424  etransclem44  46706  etransclem45  46707  etransclem47  46709  hoissre  46972  hoiprodcl  46975  ovnsubaddlem1  46998  ovnhoilem2  47030  hoicoto2  47033  ovncvr2  47039  opnvonmbllem2  47061  ovolval2lem  47071  ovolval3  47075  ovolval4lem1  47077  ovolval4lem2  47078  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  smfpimbor1lem1  47226  2arymaptf  49122  rrx2xpref1o  49188  elxpcbasex1ALT  49718  swapf2f1oa  49746  swapfida  49749  fuco2eld2  49783  fucoco2  49827  pgindlem  50184