Theorem xp1st 7931

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 5643	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3445	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3445	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7909	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2821	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 478	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 714	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1934	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540  ∃wex 1780   ∈ wcel 2105  ⟨cop 4579   × cxp 5618  ‘cfv 6479  1^st c1st 7897

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372  ax-un 7650

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-mpt 5176  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-iota 6431  df-fun 6481  df-fv 6487  df-1st 7899

This theorem is referenced by:  el2xptp0  7946  offval22  7996  fimaproj  8043  xpf1o  9004  xpmapenlem  9009  mapunen  9011  unxpwdom2  9445  djulf1o  9769  djurf1o  9770  djur  9776  eldju1st  9780  r0weon  9869  infxpenlem  9870  fseqdom  9883  iundom2g  10397  enqbreq2  10777  nqereu  10786  addpqf  10801  mulpqf  10803  adderpqlem  10811  mulerpqlem  10812  addassnq  10815  mulassnq  10816  distrnq  10818  mulidnq  10820  recmulnq  10821  ltsonq  10826  lterpq  10827  ltanq  10828  ltmnq  10829  ltexnq  10832  archnq  10837  elreal2  10989  cnref1o  12826  fsum2dlem  15581  fsumcom2  15585  ackbijnn  15639  fprod2dlem  15789  fprodcom2  15793  ruclem6  16043  ruclem8  16045  ruclem9  16046  ruclem10  16047  ruclem11  16048  ruclem12  16049  eucalgval  16384  eucalginv  16386  eucalglt  16387  eucalg  16389  xpsff1o  17375  comfffval2  17507  comfeq  17512  idfucl  17693  funcpropd  17713  fucpropd  17792  xpccatid  18002  1stfcl  18011  2ndfcl  18012  xpcpropd  18023  hofcl  18074  hofpropd  18082  yonedalem3  18095  lsmhash  19406  gsum2dlem2  19667  evlslem4  21390  mdetunilem9  21875  tx2cn  22867  txdis  22889  txlly  22893  txnlly  22894  txhaus  22904  txkgen  22909  txconn  22946  txhmeo  23060  ptuncnv  23064  ptunhmeo  23065  xkohmeo  23072  utop2nei  23508  utop3cls  23509  imasdsf1olem  23632  cnheiborlem  24223  caubl  24578  caublcls  24579  bcthlem2  24595  bcthlem4  24597  bcthlem5  24598  ovolficcss  24739  ovoliunlem1  24772  ovoliunlem2  24773  ovolicc2lem1  24787  ovolicc2lem2  24788  ovolicc2lem4  24790  ovolicc2lem5  24791  dyadmbl  24870  fsumvma  26467  lgsquadlem1  26634  lgsquadlem2  26635  opreu2reuALT  31113  disjxpin  31214  fsumiunle  31430  gsummpt2d  31596  cnre2csqima  32159  tpr2rico  32160  esum2dlem  32358  esumiun  32360  2ndmbfm  32528  sxbrsigalem0  32538  dya2iocnrect  32548  sibfof  32607  sitgaddlemb  32615  hgt750lemb  32936  satefvfmla0  33679  msubff  33791  msubco  33792  mpst123  33801  msubvrs  33821  funtransport  34429  filnetlem3  34665  elxp8  35647  finixpnum  35867  poimirlem4  35886  poimirlem5  35887  poimirlem6  35888  poimirlem7  35889  poimirlem8  35890  poimirlem9  35891  poimirlem10  35892  poimirlem11  35893  poimirlem12  35894  poimirlem13  35895  poimirlem14  35896  poimirlem15  35897  poimirlem16  35898  poimirlem17  35899  poimirlem18  35900  poimirlem19  35901  poimirlem20  35902  poimirlem21  35903  poimirlem22  35904  poimirlem25  35907  poimirlem26  35908  poimirlem27  35909  poimirlem29  35911  poimirlem30  35912  poimirlem31  35913  poimirlem32  35914  heicant  35917  mblfinlem1  35919  mblfinlem2  35920  ftc2nc  35964  heiborlem8  36081  dvhb1dimN  39254  dvhvaddcl  39363  dvhvaddcomN  39364  dvhvscacl  39371  dvhgrp  39375  dvhlveclem  39376  dibelval1st  39417  dicelval1stN  39456  aks6d1c2p1  40353  rmxypairf1o  40996  frmx  40998  cnmetcoval  43069  dvnprodlem1  43823  dvnprodlem2  43824  volicoff  43872  voliooicof  43873  etransclem44  44155  etransclem45  44156  etransclem47  44158  hoissre  44419  hoiprodcl  44422  ovnsubaddlem1  44445  ovnhoilem2  44477  hoicoto2  44480  ovncvr2  44486  opnvonmbllem2  44508  ovolval2lem  44518  ovolval3  44522  ovolval4lem1  44524  ovolval4lem2  44525  ovolval5lem2  44528  ovnovollem1  44531  ovnovollem2  44532  smfpimbor1lem1  44673  2arymaptf  46349  rrx2xpref1o  46415