Theorem xp1st 7975

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 5655	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3446	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3446	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7953	. . . . . 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 4588   × cxp 5630  ‘cfv 6500  1^st c1st 7941

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fv 6508  df-1st 7943

This theorem is referenced by:  el2xptp0  7990  offval22  8040  fimaproj  8087  xpf1o  9079  xpmapenlem  9084  mapunen  9086  unxpwdom2  9505  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  12910  fsum2dlem  15705  fsumcom2  15709  ackbijnn  15763  fprod2dlem  15915  fprodcom2  15919  ruclem6  16172  ruclem8  16174  ruclem9  16175  ruclem10  16176  ruclem11  16177  ruclem12  16178  eucalgval  16521  eucalginv  16523  eucalglt  16524  eucalg  16526  xpsff1o  17500  comfffval2  17636  comfeq  17641  idfucl  17817  funcpropd  17838  fucpropd  17916  xpccatid  18123  1stfcl  18132  2ndfcl  18133  xpcpropd  18143  hofcl  18194  hofpropd  18202  yonedalem3  18215  lsmhash  19646  gsum2dlem2  19912  evlslem4  22043  mdetunilem9  22576  tx2cn  23566  txdis  23588  txlly  23592  txnlly  23593  txhaus  23603  txkgen  23608  txconn  23645  txhmeo  23759  ptuncnv  23763  ptunhmeo  23764  xkohmeo  23771  utop2nei  24206  utop3cls  24207  imasdsf1olem  24329  cnheiborlem  24921  caubl  25276  caublcls  25277  bcthlem2  25293  bcthlem4  25295  bcthlem5  25296  ovolficcss  25438  ovoliunlem1  25471  ovoliunlem2  25472  ovolicc2lem1  25486  ovolicc2lem2  25487  ovolicc2lem4  25489  ovolicc2lem5  25490  dyadmbl  25569  fsumvma  27192  lgsquadlem1  27359  lgsquadlem2  27360  opreu2reuALT  32562  disjxpin  32674  fsumiunle  32920  gsummpt2d  33142  gsumwrd2dccatlem  33170  conjga  33263  elrgspnlem2  33336  elrgspnsubrunlem2  33341  erler  33358  rlocaddval  33361  rlocmulval  33362  mplvrpmga  33721  cnre2csqima  34088  tpr2rico  34089  esum2dlem  34269  esumiun  34271  2ndmbfm  34438  sxbrsigalem0  34448  dya2iocnrect  34458  sibfof  34517  sitgaddlemb  34525  hgt750lemb  34833  satefvfmla0  35631  msubff  35743  msubco  35744  mpst123  35753  msubvrs  35773  funtransport  36244  filnetlem3  36593  elxp8  37615  finixpnum  37845  poimirlem4  37864  poimirlem5  37865  poimirlem6  37866  poimirlem7  37867  poimirlem8  37868  poimirlem9  37869  poimirlem10  37870  poimirlem11  37871  poimirlem12  37872  poimirlem13  37873  poimirlem14  37874  poimirlem15  37875  poimirlem16  37876  poimirlem17  37877  poimirlem18  37878  poimirlem19  37879  poimirlem20  37880  poimirlem21  37881  poimirlem22  37882  poimirlem25  37885  poimirlem26  37886  poimirlem27  37887  poimirlem29  37889  poimirlem30  37890  poimirlem31  37891  poimirlem32  37892  heicant  37895  mblfinlem1  37897  mblfinlem2  37898  ftc2nc  37942  heiborlem8  38058  dvhb1dimN  41351  dvhvaddcl  41460  dvhvaddcomN  41461  dvhvscacl  41468  dvhgrp  41472  dvhlveclem  41473  dibelval1st  41514  dicelval1stN  41553  aks6d1c2p1  42477  aks6d1c3  42482  aks6d1c4  42483  aks6d1c6lem2  42530  aks6d1c6lem4  42532  f1o2d2  42594  rmxypairf1o  43257  frmx  43259  cnmetcoval  45549  dvnprodlem1  46293  dvnprodlem2  46294  volicoff  46342  voliooicof  46343  etransclem44  46625  etransclem45  46626  etransclem47  46628  hoissre  46891  hoiprodcl  46894  ovnsubaddlem1  46917  ovnhoilem2  46949  hoicoto2  46952  ovncvr2  46958  opnvonmbllem2  46980  ovolval2lem  46990  ovolval3  46994  ovolval4lem1  46996  ovolval4lem2  46997  ovolval5lem2  47000  ovnovollem1  47003  ovnovollem2  47004  smfpimbor1lem1  47145  2arymaptf  49001  rrx2xpref1o  49067  elxpcbasex1ALT  49597  swapf2f1oa  49625  swapfida  49628  fuco2eld2  49662  fucoco2  49706  pgindlem  50063