Theorem xp1st 7720

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 5577	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3497	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3497	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 7698	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2897	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 480	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 715	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1929	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 219	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533  ∃wex 1776   ∈ wcel 2110  ⟨cop 4572   × cxp 5552  ‘cfv 6354  1^st c1st 7686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-iota 6313  df-fun 6356  df-fv 6362  df-1st 7688

This theorem is referenced by:  el2xptp0  7735  offval22  7782  fimaproj  7828  xpf1o  8678  xpmapenlem  8683  mapunen  8685  unxpwdom2  9051  djulf1o  9340  djurf1o  9341  djur  9347  eldju1st  9351  r0weon  9437  infxpenlem  9438  fseqdom  9451  iundom2g  9961  enqbreq2  10341  nqereu  10350  addpqf  10365  mulpqf  10367  adderpqlem  10375  mulerpqlem  10376  addassnq  10379  mulassnq  10380  distrnq  10382  mulidnq  10384  recmulnq  10385  ltsonq  10390  lterpq  10391  ltanq  10392  ltmnq  10393  ltexnq  10396  archnq  10401  elreal2  10553  cnref1o  12383  fsum2dlem  15124  fsumcom2  15128  ackbijnn  15182  fprod2dlem  15333  fprodcom2  15337  ruclem6  15587  ruclem8  15589  ruclem9  15590  ruclem10  15591  ruclem11  15592  ruclem12  15593  eucalgval  15925  eucalginv  15927  eucalglt  15928  eucalg  15930  xpsff1o  16839  comfffval2  16970  comfeq  16975  idfucl  17150  funcpropd  17169  fucpropd  17246  xpccatid  17437  1stfcl  17446  2ndfcl  17447  xpcpropd  17457  hofcl  17508  hofpropd  17516  yonedalem3  17529  lsmhash  18830  gsum2dlem2  19090  evlslem4  20287  mdetunilem9  21228  tx2cn  22217  txdis  22239  txlly  22243  txnlly  22244  txhaus  22254  txkgen  22259  txconn  22296  txhmeo  22410  ptuncnv  22414  ptunhmeo  22415  xkohmeo  22422  utop2nei  22858  utop3cls  22859  imasdsf1olem  22982  cnheiborlem  23557  caubl  23910  caublcls  23911  bcthlem2  23927  bcthlem4  23929  bcthlem5  23930  ovolficcss  24069  ovoliunlem1  24102  ovoliunlem2  24103  ovolicc2lem1  24117  ovolicc2lem2  24118  ovolicc2lem4  24120  ovolicc2lem5  24121  dyadmbl  24200  fsumvma  25788  lgsquadlem1  25955  lgsquadlem2  25956  opreu2reuALT  30239  disjxpin  30337  fsumiunle  30545  gsummpt2d  30687  cnre2csqima  31154  tpr2rico  31155  esum2dlem  31351  esumiun  31353  2ndmbfm  31519  sxbrsigalem0  31529  dya2iocnrect  31539  sibfof  31598  sitgaddlemb  31606  hgt750lemb  31927  satefvfmla0  32665  msubff  32777  msubco  32778  mpst123  32787  msubvrs  32807  funtransport  33492  filnetlem3  33728  elxp8  34651  finixpnum  34876  poimirlem4  34895  poimirlem5  34896  poimirlem6  34897  poimirlem7  34898  poimirlem8  34899  poimirlem9  34900  poimirlem10  34901  poimirlem11  34902  poimirlem12  34903  poimirlem13  34904  poimirlem14  34905  poimirlem15  34906  poimirlem16  34907  poimirlem17  34908  poimirlem18  34909  poimirlem19  34910  poimirlem20  34911  poimirlem21  34912  poimirlem22  34913  poimirlem25  34916  poimirlem26  34917  poimirlem27  34918  poimirlem29  34920  poimirlem30  34921  poimirlem31  34922  poimirlem32  34923  heicant  34926  mblfinlem1  34928  mblfinlem2  34929  ftc2nc  34975  heiborlem8  35095  dvhb1dimN  38121  dvhvaddcl  38230  dvhvaddcomN  38231  dvhvscacl  38238  dvhgrp  38242  dvhlveclem  38243  dibelval1st  38284  dicelval1stN  38323  rmxypairf1o  39506  frmx  39508  cnmetcoval  41463  dvnprodlem1  42229  dvnprodlem2  42230  volicoff  42279  voliooicof  42280  etransclem44  42562  etransclem45  42563  etransclem47  42565  hoissre  42825  hoiprodcl  42828  ovnsubaddlem1  42851  ovnhoilem2  42883  hoicoto2  42886  ovncvr2  42892  opnvonmbllem2  42914  ovolval2lem  42924  ovolval3  42928  ovolval4lem1  42930  ovolval4lem2  42931  ovolval5lem2  42934  ovnovollem1  42937  ovnovollem2  42938  smfpimbor1lem1  43072  rrx2xpref1o  44704