Theorem xp1st 8034

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 5704	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3465	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3465	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 8012	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2810	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 476	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 715	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1927	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533  ∃wex 1773   ∈ wcel 2098  ⟨cop 4638   × cxp 5679  ‘cfv 6553  1^st c1st 8000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432  ax-un 7745

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5579  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-iota 6505  df-fun 6555  df-fv 6561  df-1st 8002

This theorem is referenced by:  el2xptp0  8049  offval22  8101  fimaproj  8148  xpf1o  9176  xpmapenlem  9181  mapunen  9183  unxpwdom2  9627  djulf1o  9951  djurf1o  9952  djur  9958  eldju1st  9962  r0weon  10051  infxpenlem  10052  fseqdom  10065  iundom2g  10579  enqbreq2  10959  nqereu  10968  addpqf  10983  mulpqf  10985  adderpqlem  10993  mulerpqlem  10994  addassnq  10997  mulassnq  10998  distrnq  11000  mulidnq  11002  recmulnq  11003  ltsonq  11008  lterpq  11009  ltanq  11010  ltmnq  11011  ltexnq  11014  archnq  11019  elreal2  11171  cnref1o  13016  fsum2dlem  15769  fsumcom2  15773  ackbijnn  15827  fprod2dlem  15977  fprodcom2  15981  ruclem6  16232  ruclem8  16234  ruclem9  16235  ruclem10  16236  ruclem11  16237  ruclem12  16238  eucalgval  16578  eucalginv  16580  eucalglt  16581  eucalg  16583  xpsff1o  17577  comfffval2  17709  comfeq  17714  idfucl  17895  funcpropd  17917  fucpropd  17997  xpccatid  18207  1stfcl  18216  2ndfcl  18217  xpcpropd  18228  hofcl  18279  hofpropd  18287  yonedalem3  18300  lsmhash  19698  gsum2dlem2  19964  evlslem4  22081  mdetunilem9  22605  tx2cn  23597  txdis  23619  txlly  23623  txnlly  23624  txhaus  23634  txkgen  23639  txconn  23676  txhmeo  23790  ptuncnv  23794  ptunhmeo  23795  xkohmeo  23802  utop2nei  24238  utop3cls  24239  imasdsf1olem  24362  cnheiborlem  24963  caubl  25319  caublcls  25320  bcthlem2  25336  bcthlem4  25338  bcthlem5  25339  ovolficcss  25481  ovoliunlem1  25514  ovoliunlem2  25515  ovolicc2lem1  25529  ovolicc2lem2  25530  ovolicc2lem4  25532  ovolicc2lem5  25533  dyadmbl  25612  fsumvma  27234  lgsquadlem1  27401  lgsquadlem2  27402  opreu2reuALT  32396  disjxpin  32499  fsumiunle  32719  gsummpt2d  32895  erler  33097  rlocaddval  33100  rlocmulval  33101  cnre2csqima  33682  tpr2rico  33683  esum2dlem  33881  esumiun  33883  2ndmbfm  34051  sxbrsigalem0  34061  dya2iocnrect  34071  sibfof  34130  sitgaddlemb  34138  hgt750lemb  34458  satefvfmla0  35198  msubff  35310  msubco  35311  mpst123  35320  msubvrs  35340  funtransport  35803  filnetlem3  36040  elxp8  37026  finixpnum  37254  poimirlem4  37273  poimirlem5  37274  poimirlem6  37275  poimirlem7  37276  poimirlem8  37277  poimirlem9  37278  poimirlem10  37279  poimirlem11  37280  poimirlem12  37281  poimirlem13  37282  poimirlem14  37283  poimirlem15  37284  poimirlem16  37285  poimirlem17  37286  poimirlem18  37287  poimirlem19  37288  poimirlem20  37289  poimirlem21  37290  poimirlem22  37291  poimirlem25  37294  poimirlem26  37295  poimirlem27  37296  poimirlem29  37298  poimirlem30  37299  poimirlem31  37300  poimirlem32  37301  heicant  37304  mblfinlem1  37306  mblfinlem2  37307  ftc2nc  37351  heiborlem8  37467  dvhb1dimN  40633  dvhvaddcl  40742  dvhvaddcomN  40743  dvhvscacl  40750  dvhgrp  40754  dvhlveclem  40755  dibelval1st  40796  dicelval1stN  40835  aks6d1c2p1  41764  aks6d1c3  41769  aks6d1c4  41770  aks6d1c6lem2  41817  aks6d1c6lem4  41819  f1o2d2  41900  rmxypairf1o  42506  frmx  42508  cnmetcoval  44746  dvnprodlem1  45504  dvnprodlem2  45505  volicoff  45553  voliooicof  45554  etransclem44  45836  etransclem45  45837  etransclem47  45839  hoissre  46102  hoiprodcl  46105  ovnsubaddlem1  46128  ovnhoilem2  46160  hoicoto2  46163  ovncvr2  46169  opnvonmbllem2  46191  ovolval2lem  46201  ovolval3  46205  ovolval4lem1  46207  ovolval4lem2  46208  ovolval5lem2  46211  ovnovollem1  46214  ovnovollem2  46215  smfpimbor1lem1  46356  2arymaptf  47977  rrx2xpref1o  48043  pgindlem  48398