Theorem xp1st 7348

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 5272	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3354	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3354	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7326	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2835	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 463	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 690	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 2012	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 207	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631  ∃wex 1852   ∈ wcel 2145  ⟨cop 4323   × cxp 5248  ‘cfv 6032  1^st c1st 7314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3589  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-iota 5995  df-fun 6034  df-fv 6040  df-1st 7316

This theorem is referenced by:  el2xptp0  7362  offval22  7405  xpf1o  8279  xpmapenlem  8284  mapunen  8286  unxpwdom2  8650  djulf1o  8939  djurf1o  8940  djur  8946  eldju1st  8950  r0weon  9036  infxpenlem  9037  fseqdom  9050  iundom2g  9565  enqbreq2  9945  nqereu  9954  addpqf  9969  mulpqf  9971  adderpqlem  9979  mulerpqlem  9980  addassnq  9983  mulassnq  9984  distrnq  9986  mulidnq  9988  recmulnq  9989  ltsonq  9994  lterpq  9995  ltanq  9996  ltmnq  9997  ltexnq  10000  archnq  10005  elreal2  10156  cnref1o  12031  fsum2dlem  14710  fsumcom2  14714  ackbijnn  14768  fprod2dlem  14918  fprodcom2  14922  ruclem6  15171  ruclem8  15173  ruclem9  15174  ruclem10  15175  ruclem11  15176  ruclem12  15177  eucalgval  15504  eucalginv  15506  eucalglt  15507  eucalg  15509  xpsff1o  16437  comfffval2  16569  comfeq  16574  idfucl  16749  funcpropd  16768  fucpropd  16845  xpccatid  17037  1stfcl  17046  2ndfcl  17047  xpcpropd  17057  hofcl  17108  hofpropd  17116  yonedalem3  17129  lsmhash  18326  gsum2dlem2  18578  evlslem4  19724  mdetunilem9  20645  tx2cn  21635  txdis  21657  txlly  21661  txnlly  21662  txhaus  21672  txkgen  21677  txconn  21714  txhmeo  21828  ptuncnv  21832  ptunhmeo  21833  xkohmeo  21840  utop2nei  22275  utop3cls  22276  imasdsf1olem  22399  cnheiborlem  22974  caubl  23326  caublcls  23327  bcthlem2  23342  bcthlem4  23344  bcthlem5  23345  ovolficcss  23458  ovoliunlem1  23491  ovoliunlem2  23492  ovolicc2lem1  23506  ovolicc2lem2  23507  ovolicc2lem4  23509  ovolicc2lem5  23510  dyadmbl  23589  fsumvma  25160  lgsquadlem1  25327  lgsquadlem2  25328  disjxpin  29740  fsumiunle  29916  gsummpt2d  30122  fimaproj  30241  cnre2csqima  30298  tpr2rico  30299  esum2dlem  30495  esumiun  30497  2ndmbfm  30664  sxbrsigalem0  30674  dya2iocnrect  30684  sibfof  30743  sitgaddlemb  30751  hgt750lemb  31075  msubff  31766  msubco  31767  mpst123  31776  msubvrs  31796  funtransport  32476  filnetlem3  32713  elxp8  33557  finixpnum  33728  poimirlem4  33747  poimirlem5  33748  poimirlem6  33749  poimirlem7  33750  poimirlem8  33751  poimirlem9  33752  poimirlem10  33753  poimirlem11  33754  poimirlem12  33755  poimirlem13  33756  poimirlem14  33757  poimirlem15  33758  poimirlem16  33759  poimirlem17  33760  poimirlem18  33761  poimirlem19  33762  poimirlem20  33763  poimirlem21  33764  poimirlem22  33765  poimirlem25  33768  poimirlem26  33769  poimirlem27  33770  poimirlem29  33772  poimirlem30  33773  poimirlem31  33774  poimirlem32  33775  heicant  33778  mblfinlem1  33780  mblfinlem2  33781  ftc2nc  33827  heiborlem8  33950  dvhb1dimN  36796  dvhvaddcl  36906  dvhvaddcomN  36907  dvhvscacl  36914  dvhgrp  36918  dvhlveclem  36919  dibelval1st  36960  dicelval1stN  36999  rmxypairf1o  38003  frmx  38005  cnmetcoval  39913  dvnprodlem1  40680  dvnprodlem2  40681  volicoff  40730  voliooicof  40731  etransclem44  41013  etransclem45  41014  etransclem47  41016  hoissre  41279  hoiprodcl  41282  ovnsubaddlem1  41305  ovnhoilem2  41337  hoicoto2  41340  ovncvr2  41346  opnvonmbllem2  41368  ovolval2lem  41378  ovolval3  41382  ovolval4lem1  41384  ovolval4lem2  41385  ovolval5lem2  41388  ovnovollem1  41391  ovnovollem2  41392  smfpimbor1lem1  41526