Theorem xp1st 7948

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 5637	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3438	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3438	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7926	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2814	. . . . 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 2110  ⟨cop 4580   × cxp 5612  ‘cfv 6477  1^st c1st 7914

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 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663

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 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6433  df-fun 6479  df-fv 6485  df-1st 7916

This theorem is referenced by:  el2xptp0  7963  offval22  8013  fimaproj  8060  xpf1o  9047  xpmapenlem  9052  mapunen  9054  unxpwdom2  9469  djulf1o  9797  djurf1o  9798  djur  9804  eldju1st  9808  r0weon  9895  infxpenlem  9896  fseqdom  9909  iundom2g  10423  enqbreq2  10803  nqereu  10812  addpqf  10827  mulpqf  10829  adderpqlem  10837  mulerpqlem  10838  addassnq  10841  mulassnq  10842  distrnq  10844  mulidnq  10846  recmulnq  10847  ltsonq  10852  lterpq  10853  ltanq  10854  ltmnq  10855  ltexnq  10858  archnq  10863  elreal2  11015  cnref1o  12875  fsum2dlem  15669  fsumcom2  15673  ackbijnn  15727  fprod2dlem  15879  fprodcom2  15883  ruclem6  16136  ruclem8  16138  ruclem9  16139  ruclem10  16140  ruclem11  16141  ruclem12  16142  eucalgval  16485  eucalginv  16487  eucalglt  16488  eucalg  16490  xpsff1o  17463  comfffval2  17599  comfeq  17604  idfucl  17780  funcpropd  17801  fucpropd  17879  xpccatid  18086  1stfcl  18095  2ndfcl  18096  xpcpropd  18106  hofcl  18157  hofpropd  18165  yonedalem3  18178  lsmhash  19610  gsum2dlem2  19876  evlslem4  22004  mdetunilem9  22528  tx2cn  23518  txdis  23540  txlly  23544  txnlly  23545  txhaus  23555  txkgen  23560  txconn  23597  txhmeo  23711  ptuncnv  23715  ptunhmeo  23716  xkohmeo  23723  utop2nei  24158  utop3cls  24159  imasdsf1olem  24281  cnheiborlem  24873  caubl  25228  caublcls  25229  bcthlem2  25245  bcthlem4  25247  bcthlem5  25248  ovolficcss  25390  ovoliunlem1  25423  ovoliunlem2  25424  ovolicc2lem1  25438  ovolicc2lem2  25439  ovolicc2lem4  25441  ovolicc2lem5  25442  dyadmbl  25521  fsumvma  27144  lgsquadlem1  27311  lgsquadlem2  27312  opreu2reuALT  32446  disjxpin  32558  fsumiunle  32802  gsummpt2d  33019  gsumwrd2dccatlem  33036  conjga  33129  elrgspnlem2  33200  elrgspnsubrunlem2  33205  erler  33222  rlocaddval  33225  rlocmulval  33226  mplvrpmga  33565  cnre2csqima  33914  tpr2rico  33915  esum2dlem  34095  esumiun  34097  2ndmbfm  34264  sxbrsigalem0  34274  dya2iocnrect  34284  sibfof  34343  sitgaddlemb  34351  hgt750lemb  34659  satefvfmla0  35430  msubff  35542  msubco  35543  mpst123  35552  msubvrs  35572  funtransport  36044  filnetlem3  36393  elxp8  37384  finixpnum  37624  poimirlem4  37643  poimirlem5  37644  poimirlem6  37645  poimirlem7  37646  poimirlem8  37647  poimirlem9  37648  poimirlem10  37649  poimirlem11  37650  poimirlem12  37651  poimirlem13  37652  poimirlem14  37653  poimirlem15  37654  poimirlem16  37655  poimirlem17  37656  poimirlem18  37657  poimirlem19  37658  poimirlem20  37659  poimirlem21  37660  poimirlem22  37661  poimirlem25  37664  poimirlem26  37665  poimirlem27  37666  poimirlem29  37668  poimirlem30  37669  poimirlem31  37670  poimirlem32  37671  heicant  37674  mblfinlem1  37676  mblfinlem2  37677  ftc2nc  37721  heiborlem8  37837  dvhb1dimN  41004  dvhvaddcl  41113  dvhvaddcomN  41114  dvhvscacl  41121  dvhgrp  41125  dvhlveclem  41126  dibelval1st  41167  dicelval1stN  41206  aks6d1c2p1  42130  aks6d1c3  42135  aks6d1c4  42136  aks6d1c6lem2  42183  aks6d1c6lem4  42185  f1o2d2  42245  rmxypairf1o  42923  frmx  42925  cnmetcoval  45218  dvnprodlem1  45963  dvnprodlem2  45964  volicoff  46012  voliooicof  46013  etransclem44  46295  etransclem45  46296  etransclem47  46298  hoissre  46561  hoiprodcl  46564  ovnsubaddlem1  46587  ovnhoilem2  46619  hoicoto2  46622  ovncvr2  46628  opnvonmbllem2  46650  ovolval2lem  46660  ovolval3  46664  ovolval4lem1  46666  ovolval4lem2  46667  ovolval5lem2  46670  ovnovollem1  46673  ovnovollem2  46674  smfpimbor1lem1  46815  2arymaptf  48663  rrx2xpref1o  48729  elxpcbasex1ALT  49260  swapf2f1oa  49288  swapfida  49291  fuco2eld2  49325  fucoco2  49369  pgindlem  49726