Theorem xp1st 7991

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 5663	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3452	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3452	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7969	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2841	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 480	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 725	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1946	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 219	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1554  ∃wex 1793   ∈ wcel 2136  ⟨cop 4582   × cxp 5638  ‘cfv 6510  1^st c1st 7957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pr 5384  ax-un 7707

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-iota 6466  df-fun 6512  df-fv 6518  df-1st 7959

This theorem is referenced by:  el2xptp0  8006  offval22  8055  mpof1o2d  8093  fimaproj  8103  xpf1o  9100  xpmapenlem  9105  mapunen  9107  unxpwdom2  9526  djulf1o  9860  djurf1o  9861  djur  9867  eldju1st  9871  r0weon  9958  infxpenlem  9959  fseqdom  9972  iundom2g  10487  enqbreq2  10868  nqereu  10877  addpqf  10892  mulpqf  10894  adderpqlem  10902  mulerpqlem  10903  addassnq  10906  mulassnq  10907  distrnq  10909  mulidnq  10911  recmulnq  10912  ltsonq  10917  lterpq  10918  ltanq  10919  ltmnq  10920  ltexnq  10923  archnq  10928  elreal2  11080  cnref1o  12976  fsum2dlem  15773  fsumcom2  15777  ackbijnn  15834  fprod2dlem  15986  fprodcom2  15990  ruclem6  16243  ruclem8  16245  ruclem9  16246  ruclem10  16247  ruclem11  16248  ruclem12  16249  eucalgval  16592  eucalginv  16594  eucalglt  16595  eucalg  16597  xpsff1o  17573  comfffval2  17709  comfeq  17714  idfucl  17890  funcpropd  17911  fucpropd  17989  xpccatid  18196  1stfcl  18205  2ndfcl  18206  xpcpropd  18216  hofcl  18267  hofpropd  18275  yonedalem3  18288  lsmhash  19721  gsum2dlem2  19987  evlslem4  22102  mdetunilem9  22653  tx2cn  23643  txdis  23665  txlly  23669  txnlly  23670  txhaus  23680  txkgen  23685  txconn  23722  txhmeo  23836  ptuncnv  23840  ptunhmeo  23841  xkohmeo  23848  utop2nei  24283  utop3cls  24284  imasdsf1olem  24406  cnheiborlem  24989  caubl  25343  caublcls  25344  bcthlem2  25360  bcthlem4  25362  bcthlem5  25363  ovolficcss  25504  ovoliunlem1  25537  ovoliunlem2  25538  ovolicc2lem1  25552  ovolicc2lem2  25553  ovolicc2lem4  25555  ovolicc2lem5  25556  dyadmbl  25635  fsumvma  27247  lgsquadlem1  27414  lgsquadlem2  27415  opreu2reuALT  32617  disjxpin  32730  fsumiunle  32974  gsummpt2d  33183  gsumwrd2dccatlem  33211  conjga  33304  elrgspnlem2  33378  elrgspnsubrunlem2  33383  erler  33400  rlocaddval  33404  rlocmulval  33405  mplvrpmga  33796  cnre2csqima  34162  tpr2rico  34163  esum2dlem  34343  esumiun  34345  2ndmbfm  34512  sxbrsigalem0  34522  dya2iocnrect  34532  sibfof  34591  sitgaddlemb  34599  hgt750lemb  34907  satefvfmla0  35716  msubff  35828  msubco  35829  mpst123  35838  msubvrs  35858  funtransport  36329  filnetlem3  36688  elxp8  37813  finixpnum  38052  poimirlem4  38071  poimirlem5  38072  poimirlem6  38073  poimirlem7  38074  poimirlem8  38075  poimirlem9  38076  poimirlem10  38077  poimirlem11  38078  poimirlem12  38079  poimirlem13  38080  poimirlem14  38081  poimirlem15  38082  poimirlem16  38083  poimirlem17  38084  poimirlem18  38085  poimirlem19  38086  poimirlem20  38087  poimirlem21  38088  poimirlem22  38089  poimirlem25  38092  poimirlem26  38093  poimirlem27  38094  poimirlem29  38096  poimirlem30  38097  poimirlem31  38098  poimirlem32  38099  heicant  38102  mblfinlem1  38104  mblfinlem2  38105  ftc2nc  38149  heiborlem8  38265  dvhb1dimN  41558  dvhvaddcl  41667  dvhvaddcomN  41668  dvhvscacl  41675  dvhgrp  41679  dvhlveclem  41680  dibelval1st  41721  dicelval1stN  41760  aks6d1c2p1  42683  aks6d1c3  42688  aks6d1c4  42689  aks6d1c6lem2  42736  aks6d1c6lem4  42738  rmxypairf1o  43436  frmx  43438  cnmetcoval  45727  dvnprodlem1  46468  dvnprodlem2  46469  volicoff  46517  voliooicof  46518  etransclem44  46800  etransclem45  46801  etransclem47  46803  hoissre  47066  hoiprodcl  47069  ovnsubaddlem1  47092  ovnhoilem2  47124  hoicoto2  47127  ovncvr2  47133  opnvonmbllem2  47155  ovolval2lem  47165  ovolval3  47169  ovolval4lem1  47171  ovolval4lem2  47172  ovolval5lem2  47175  ovnovollem1  47178  ovnovollem2  47179  smfpimbor1lem1  47320  2arymaptf  49222  rrx2xpref1o  49288  elxpcbasex1ALT  49818  swapf2f1oa  49846  swapfida  49849  fuco2eld2  49883  fucoco2  49927  pgindlem  50284