Theorem xp2nd 7864

Description: Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
xp2nd	⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Proof of Theorem xp2nd

Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 5612	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3436	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3436	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7842	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2823	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 478	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 713	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1935	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ⟨cop 4567   × cxp 5587  ‘cfv 6433  2^nd c2nd 7830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6391  df-fun 6435  df-fv 6441  df-2nd 7832

This theorem is referenced by:  offval22  7928  fimaproj  7976  disjen  8921  xpf1o  8926  xpmapenlem  8931  mapunen  8933  djur  9677  r0weon  9768  infxpenlem  9769  fseqdom  9782  axcc2lem  10192  iunfo  10295  iundom2g  10296  enqbreq2  10676  nqereu  10685  addpqf  10700  mulpqf  10702  adderpqlem  10710  mulerpqlem  10711  addassnq  10714  mulassnq  10715  distrnq  10717  mulidnq  10719  recmulnq  10720  ltsonq  10725  lterpq  10726  ltanq  10727  ltmnq  10728  ltexnq  10731  archnq  10736  elreal2  10888  cnref1o  12725  fsumcom2  15486  fprodcom2  15694  ruclem6  15944  ruclem8  15946  ruclem9  15947  ruclem10  15948  ruclem12  15950  eucalgval  16287  eucalginv  16289  eucalglt  16290  eucalgcvga  16291  eucalg  16292  xpsff1o  17278  comfffval2  17410  comfeq  17415  idfucl  17596  funcpropd  17616  fucpropd  17695  xpccatid  17905  1stfcl  17914  2ndfcl  17915  xpcpropd  17926  hofcl  17977  hofpropd  17985  yonedalem3  17998  lsmhash  19311  gsum2dlem2  19572  dprd2da  19645  evlslem4  21284  mdetunilem9  21769  tx1cn  22760  txdis  22783  txlly  22787  txnlly  22788  txhaus  22798  txkgen  22803  txconn  22840  txhmeo  22954  ptuncnv  22958  ptunhmeo  22959  xkohmeo  22966  utop2nei  23402  utop3cls  23403  imasdsf1olem  23526  cnheiborlem  24117  caubl  24472  caublcls  24473  bcthlem2  24489  bcthlem4  24491  bcthlem5  24492  ovolficcss  24633  ovoliunlem1  24666  ovoliunlem2  24667  ovolicc2lem1  24681  ovolicc2lem2  24682  ovolicc2lem3  24683  ovolicc2lem4  24684  ovolicc2lem5  24685  dyadmbl  24764  fsumvma  26361  opreu2reuALT  30825  disjxpin  30927  2ndimaxp  30984  2ndresdju  30986  fsumiunle  31143  gsummpt2d  31309  cnre2csqima  31861  tpr2rico  31862  esum2dlem  32060  esumiun  32062  1stmbfm  32227  dya2iocnrect  32248  sibfof  32307  sitgaddlemb  32315  hgt750lemb  32636  satefvfmla0  33380  mvrsfpw  33468  msubff  33492  msubco  33493  msubvrs  33522  elxp8  35542  finixpnum  35762  poimirlem4  35781  poimirlem5  35782  poimirlem6  35783  poimirlem7  35784  poimirlem8  35785  poimirlem9  35786  poimirlem10  35787  poimirlem11  35788  poimirlem12  35789  poimirlem13  35790  poimirlem14  35791  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem18  35795  poimirlem19  35796  poimirlem20  35797  poimirlem21  35798  poimirlem22  35799  poimirlem25  35802  poimirlem26  35803  poimirlem27  35804  poimirlem29  35806  poimirlem31  35808  heicant  35812  mblfinlem1  35814  mblfinlem2  35815  ftc2nc  35859  heiborlem8  35976  dvhfvadd  39105  dvhvaddcl  39109  dvhvaddcomN  39110  dvhvaddass  39111  dvhvscacl  39117  dvhgrp  39121  dvhlveclem  39122  dibelval2nd  39166  dicelval2nd  39203  rmxypairf1o  40733  frmy  40736  cnmetcoval  42742  dvnprodlem1  43487  dvnprodlem2  43488  volicoff  43536  voliooicof  43537  etransclem44  43819  etransclem45  43820  etransclem47  43822  hoissre  44082  hoiprodcl  44085  ovnsubaddlem1  44108  ovnhoilem2  44140  hoicoto2  44143  ovncvr2  44149  opnvonmbllem2  44171  ovolval2lem  44181  ovolval3  44185  ovolval4lem1  44187  ovolval4lem2  44188  ovolval5lem2  44191  ovnovollem1  44194  ovnovollem2  44195  smfpimbor1lem1  44332  2arymaptf  45998  rrx2xpref1o  46064