Theorem xp1st 8033

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 5673	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3454	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3454	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 8011	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2845	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 483	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 730	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1964	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ⟨cop 4589   × cxp 5648  ‘cfv 6538  1^st c1st 7999

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-1st 8001

This theorem is used by:  el2xptp0  8047  offval22  8099  mpof1o2d  8137  fimaproj  8152  xpf1o  9159  xpmapenlem  9164  mapunen  9166  unxpwdom2  9583  djulf1o  9994  djurf1o  9995  djur  10001  eldju1st  10005  r0weon  10092  infxpenlem  10093  fseqdom  10106  iundom2g  10625  enqbreq2  11006  nqereu  11015  addpqf  11030  mulpqf  11032  adderpqlem  11040  mulerpqlem  11041  addassnq  11044  mulassnq  11045  distrnq  11047  mulidnq  11049  recmulnq  11050  ltsonq  11055  lterpq  11056  ltanq  11057  ltmnq  11058  ltexnq  11061  archnq  11066  elreal2  11218  cnref1o  13114  fsum2dlem  15937  fsumcom2  15941  ackbijnn  15998  fprod2dlem  16148  fprodcom2  16152  ruclem6  16404  ruclem8  16406  ruclem9  16407  ruclem10  16408  ruclem11  16409  ruclem12  16410  eucalgval  16758  eucalginv  16760  eucalglt  16761  eucalg  16763  xpsff1o  17740  comfffval2  17876  comfeq  17881  idfucl  18057  funcpropd  18078  fucpropd  18156  xpccatid  18363  1stfcl  18372  2ndfcl  18373  xpcpropd  18383  hofcl  18434  hofpropd  18442  yonedalem3  18455  lsmhash  19920  gsum2dlem2  20186  evlslem4  22386  mdetunilem9  22936  tx2cn  23930  txdis  23952  txlly  23956  txnlly  23957  txhaus  23967  txkgen  23972  txconn  24009  txhmeo  24123  ptuncnv  24127  ptunhmeo  24128  xkohmeo  24135  utop2nei  24570  utop3cls  24571  imasdsf1olem  24693  cnheiborlem  25276  caubl  25630  caublcls  25631  bcthlem2  25647  bcthlem4  25649  bcthlem5  25650  ovolficcss  25791  ovoliunlem1  25824  ovoliunlem2  25825  ovolicc2lem1  25839  ovolicc2lem2  25840  ovolicc2lem4  25842  ovolicc2lem5  25843  dyadmbl  25922  fsumvma  27541  lgsquadlem1  27708  lgsquadlem2  27709  opreu2reuALT  33116  disjxpin  33225  fsumiunle  33463  gsummpt2d  33653  gsumwrd2dccatlem  33681  conjga  33774  elrgspnlem2  33847  elrgspnsubrunlem2  33852  erler  33869  rlocaddval  33873  rlocmulval  33874  mplvrpmga  34220  cnre2csqima  34586  tpr2rico  34587  esum2dlem  34767  esumiun  34769  2ndmbfm  34936  sxbrsigalem0  34946  dya2iocnrect  34956  sibfof  35015  sitgaddlemb  35023  hgt750lemb  35328  satefvfmla0  36252  msubff  36364  msubco  36365  mpst123  36374  msubvrs  36394  funtransport  36871  filnetlem3  37243  elxp8  38370  finixpnum  38604  poimirlem4  38618  poimirlem5  38619  poimirlem6  38620  poimirlem7  38621  poimirlem8  38622  poimirlem9  38623  poimirlem10  38624  poimirlem11  38625  poimirlem12  38626  poimirlem13  38627  poimirlem14  38628  poimirlem15  38629  poimirlem16  38630  poimirlem17  38631  poimirlem18  38632  poimirlem19  38633  poimirlem20  38634  poimirlem21  38635  poimirlem22  38636  poimirlem25  38639  poimirlem26  38640  poimirlem27  38641  poimirlem29  38643  poimirlem30  38644  poimirlem31  38645  poimirlem32  38646  heicant  38649  mblfinlem1  38651  mblfinlem2  38652  ftc2nc  38696  heiborlem8  38828  dvhb1dimN  42119  dvhvaddcl  42228  dvhvaddcomN  42229  dvhvscacl  42236  dvhgrp  42240  dvhlveclem  42241  dibelval1st  42282  dicelval1stN  42321  aks6d1c2p1  43244  aks6d1c3  43249  aks6d1c4  43250  aks6d1c6lem2  43297  aks6d1c6lem4  43299  rmxypairf1o  43994  frmx  43996  cnmetcoval  46292  dvnprodlem1  47032  dvnprodlem2  47033  volicoff  47081  voliooicof  47082  etransclem44  47364  etransclem45  47365  etransclem47  47367  hoissre  47630  hoiprodcl  47633  ovnsubaddlem1  47656  ovnhoilem2  47688  hoicoto2  47691  ovncvr2  47697  opnvonmbllem2  47719  ovolval2lem  47729  ovolval3  47733  ovolval4lem1  47735  ovolval4lem2  47736  ovolval5lem2  47739  ovnovollem1  47742  ovnovollem2  47743  smfpimbor1lem1  47884  2arymaptf  49840  rrx2xpref1o  49906  elxpcbasex1ALT  50433  swapf2f1oa  50461  swapfida  50464  fuco2eld2  50498  fucoco2  50542  pgindlem  50884