Theorem xp1st 7771

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 5559	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3402	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3402	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7749	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2815	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 481	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 717	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1940	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2112  ⟨cop 4533   × cxp 5534  ‘cfv 6358  1^st c1st 7737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-iota 6316  df-fun 6360  df-fv 6366  df-1st 7739

This theorem is referenced by:  el2xptp0  7786  offval22  7834  fimaproj  7880  xpf1o  8786  xpmapenlem  8791  mapunen  8793  unxpwdom2  9182  djulf1o  9493  djurf1o  9494  djur  9500  eldju1st  9504  r0weon  9591  infxpenlem  9592  fseqdom  9605  iundom2g  10119  enqbreq2  10499  nqereu  10508  addpqf  10523  mulpqf  10525  adderpqlem  10533  mulerpqlem  10534  addassnq  10537  mulassnq  10538  distrnq  10540  mulidnq  10542  recmulnq  10543  ltsonq  10548  lterpq  10549  ltanq  10550  ltmnq  10551  ltexnq  10554  archnq  10559  elreal2  10711  cnref1o  12546  fsum2dlem  15297  fsumcom2  15301  ackbijnn  15355  fprod2dlem  15505  fprodcom2  15509  ruclem6  15759  ruclem8  15761  ruclem9  15762  ruclem10  15763  ruclem11  15764  ruclem12  15765  eucalgval  16102  eucalginv  16104  eucalglt  16105  eucalg  16107  xpsff1o  17026  comfffval2  17158  comfeq  17163  idfucl  17341  funcpropd  17361  fucpropd  17440  xpccatid  17649  1stfcl  17658  2ndfcl  17659  xpcpropd  17670  hofcl  17721  hofpropd  17729  yonedalem3  17742  lsmhash  19049  gsum2dlem2  19310  evlslem4  20988  mdetunilem9  21471  tx2cn  22461  txdis  22483  txlly  22487  txnlly  22488  txhaus  22498  txkgen  22503  txconn  22540  txhmeo  22654  ptuncnv  22658  ptunhmeo  22659  xkohmeo  22666  utop2nei  23102  utop3cls  23103  imasdsf1olem  23225  cnheiborlem  23805  caubl  24159  caublcls  24160  bcthlem2  24176  bcthlem4  24178  bcthlem5  24179  ovolficcss  24320  ovoliunlem1  24353  ovoliunlem2  24354  ovolicc2lem1  24368  ovolicc2lem2  24369  ovolicc2lem4  24371  ovolicc2lem5  24372  dyadmbl  24451  fsumvma  26048  lgsquadlem1  26215  lgsquadlem2  26216  opreu2reuALT  30498  disjxpin  30600  fsumiunle  30817  gsummpt2d  30982  cnre2csqima  31529  tpr2rico  31530  esum2dlem  31726  esumiun  31728  2ndmbfm  31894  sxbrsigalem0  31904  dya2iocnrect  31914  sibfof  31973  sitgaddlemb  31981  hgt750lemb  32302  satefvfmla0  33047  msubff  33159  msubco  33160  mpst123  33169  msubvrs  33189  funtransport  34019  filnetlem3  34255  elxp8  35228  finixpnum  35448  poimirlem4  35467  poimirlem5  35468  poimirlem6  35469  poimirlem7  35470  poimirlem8  35471  poimirlem9  35472  poimirlem10  35473  poimirlem11  35474  poimirlem12  35475  poimirlem13  35476  poimirlem14  35477  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem18  35481  poimirlem19  35482  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem25  35488  poimirlem26  35489  poimirlem27  35490  poimirlem29  35492  poimirlem30  35493  poimirlem31  35494  poimirlem32  35495  heicant  35498  mblfinlem1  35500  mblfinlem2  35501  ftc2nc  35545  heiborlem8  35662  dvhb1dimN  38686  dvhvaddcl  38795  dvhvaddcomN  38796  dvhvscacl  38803  dvhgrp  38807  dvhlveclem  38808  dibelval1st  38849  dicelval1stN  38888  rmxypairf1o  40377  frmx  40379  cnmetcoval  42356  dvnprodlem1  43105  dvnprodlem2  43106  volicoff  43154  voliooicof  43155  etransclem44  43437  etransclem45  43438  etransclem47  43440  hoissre  43700  hoiprodcl  43703  ovnsubaddlem1  43726  ovnhoilem2  43758  hoicoto2  43761  ovncvr2  43767  opnvonmbllem2  43789  ovolval2lem  43799  ovolval3  43803  ovolval4lem1  43805  ovolval4lem2  43806  ovolval5lem2  43809  ovnovollem1  43812  ovnovollem2  43813  smfpimbor1lem1  43947  2arymaptf  45614  rrx2xpref1o  45680