Theorem xp1st 7962

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 5644	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3442	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3442	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7940	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2818	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 717	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1933	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 217	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ⟨cop 4583   × cxp 5619  ‘cfv 6489  1^st c1st 7928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fv 6497  df-1st 7930

This theorem is referenced by:  el2xptp0  7977  offval22  8027  fimaproj  8074  xpf1o  9062  xpmapenlem  9067  mapunen  9069  unxpwdom2  9484  djulf1o  9815  djurf1o  9816  djur  9822  eldju1st  9826  r0weon  9913  infxpenlem  9914  fseqdom  9927  iundom2g  10441  enqbreq2  10821  nqereu  10830  addpqf  10845  mulpqf  10847  adderpqlem  10855  mulerpqlem  10856  addassnq  10859  mulassnq  10860  distrnq  10862  mulidnq  10864  recmulnq  10865  ltsonq  10870  lterpq  10871  ltanq  10872  ltmnq  10873  ltexnq  10876  archnq  10881  elreal2  11033  cnref1o  12893  fsum2dlem  15687  fsumcom2  15691  ackbijnn  15745  fprod2dlem  15897  fprodcom2  15901  ruclem6  16154  ruclem8  16156  ruclem9  16157  ruclem10  16158  ruclem11  16159  ruclem12  16160  eucalgval  16503  eucalginv  16505  eucalglt  16506  eucalg  16508  xpsff1o  17481  comfffval2  17617  comfeq  17622  idfucl  17798  funcpropd  17819  fucpropd  17897  xpccatid  18104  1stfcl  18113  2ndfcl  18114  xpcpropd  18124  hofcl  18175  hofpropd  18183  yonedalem3  18196  lsmhash  19627  gsum2dlem2  19893  evlslem4  22021  mdetunilem9  22545  tx2cn  23535  txdis  23557  txlly  23561  txnlly  23562  txhaus  23572  txkgen  23577  txconn  23614  txhmeo  23728  ptuncnv  23732  ptunhmeo  23733  xkohmeo  23740  utop2nei  24175  utop3cls  24176  imasdsf1olem  24298  cnheiborlem  24890  caubl  25245  caublcls  25246  bcthlem2  25262  bcthlem4  25264  bcthlem5  25265  ovolficcss  25407  ovoliunlem1  25440  ovoliunlem2  25441  ovolicc2lem1  25455  ovolicc2lem2  25456  ovolicc2lem4  25458  ovolicc2lem5  25459  dyadmbl  25538  fsumvma  27161  lgsquadlem1  27328  lgsquadlem2  27329  opreu2reuALT  32467  disjxpin  32579  fsumiunle  32823  gsummpt2d  33040  gsumwrd2dccatlem  33057  conjga  33150  elrgspnlem2  33221  elrgspnsubrunlem2  33226  erler  33243  rlocaddval  33246  rlocmulval  33247  mplvrpmga  33586  cnre2csqima  33935  tpr2rico  33936  esum2dlem  34116  esumiun  34118  2ndmbfm  34285  sxbrsigalem0  34295  dya2iocnrect  34305  sibfof  34364  sitgaddlemb  34372  hgt750lemb  34680  satefvfmla0  35473  msubff  35585  msubco  35586  mpst123  35595  msubvrs  35615  funtransport  36086  filnetlem3  36435  elxp8  37426  finixpnum  37655  poimirlem4  37674  poimirlem5  37675  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem9  37679  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem13  37683  poimirlem14  37684  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem18  37688  poimirlem19  37689  poimirlem20  37690  poimirlem21  37691  poimirlem22  37692  poimirlem25  37695  poimirlem26  37696  poimirlem27  37697  poimirlem29  37699  poimirlem30  37700  poimirlem31  37701  poimirlem32  37702  heicant  37705  mblfinlem1  37707  mblfinlem2  37708  ftc2nc  37752  heiborlem8  37868  dvhb1dimN  41095  dvhvaddcl  41204  dvhvaddcomN  41205  dvhvscacl  41212  dvhgrp  41216  dvhlveclem  41217  dibelval1st  41258  dicelval1stN  41297  aks6d1c2p1  42221  aks6d1c3  42226  aks6d1c4  42227  aks6d1c6lem2  42274  aks6d1c6lem4  42276  f1o2d2  42341  rmxypairf1o  43018  frmx  43020  cnmetcoval  45313  dvnprodlem1  46058  dvnprodlem2  46059  volicoff  46107  voliooicof  46108  etransclem44  46390  etransclem45  46391  etransclem47  46393  hoissre  46656  hoiprodcl  46659  ovnsubaddlem1  46682  ovnhoilem2  46714  hoicoto2  46717  ovncvr2  46723  opnvonmbllem2  46745  ovolval2lem  46755  ovolval3  46759  ovolval4lem1  46761  ovolval4lem2  46762  ovolval5lem2  46765  ovnovollem1  46768  ovnovollem2  46769  smfpimbor1lem1  46910  2arymaptf  48767  rrx2xpref1o  48833  elxpcbasex1ALT  49364  swapf2f1oa  49392  swapfida  49395  fuco2eld2  49429  fucoco2  49473  pgindlem  49830