Theorem xp2nd 7837

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 5603	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3426	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3426	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7815	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2823	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 712	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1936	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ⟨cop 4564   × cxp 5578  ‘cfv 6418  2^nd c2nd 7803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fv 6426  df-2nd 7805

This theorem is referenced by:  offval22  7899  fimaproj  7947  disjen  8870  xpf1o  8875  xpmapenlem  8880  mapunen  8882  djur  9608  r0weon  9699  infxpenlem  9700  fseqdom  9713  axcc2lem  10123  iunfo  10226  iundom2g  10227  enqbreq2  10607  nqereu  10616  addpqf  10631  mulpqf  10633  adderpqlem  10641  mulerpqlem  10642  addassnq  10645  mulassnq  10646  distrnq  10648  mulidnq  10650  recmulnq  10651  ltsonq  10656  lterpq  10657  ltanq  10658  ltmnq  10659  ltexnq  10662  archnq  10667  elreal2  10819  cnref1o  12654  fsumcom2  15414  fprodcom2  15622  ruclem6  15872  ruclem8  15874  ruclem9  15875  ruclem10  15876  ruclem12  15878  eucalgval  16215  eucalginv  16217  eucalglt  16218  eucalgcvga  16219  eucalg  16220  xpsff1o  17195  comfffval2  17327  comfeq  17332  idfucl  17512  funcpropd  17532  fucpropd  17611  xpccatid  17821  1stfcl  17830  2ndfcl  17831  xpcpropd  17842  hofcl  17893  hofpropd  17901  yonedalem3  17914  lsmhash  19226  gsum2dlem2  19487  dprd2da  19560  evlslem4  21194  mdetunilem9  21677  tx1cn  22668  txdis  22691  txlly  22695  txnlly  22696  txhaus  22706  txkgen  22711  txconn  22748  txhmeo  22862  ptuncnv  22866  ptunhmeo  22867  xkohmeo  22874  utop2nei  23310  utop3cls  23311  imasdsf1olem  23434  cnheiborlem  24023  caubl  24377  caublcls  24378  bcthlem2  24394  bcthlem4  24396  bcthlem5  24397  ovolficcss  24538  ovoliunlem1  24571  ovoliunlem2  24572  ovolicc2lem1  24586  ovolicc2lem2  24587  ovolicc2lem3  24588  ovolicc2lem4  24589  ovolicc2lem5  24590  dyadmbl  24669  fsumvma  26266  opreu2reuALT  30726  disjxpin  30828  2ndimaxp  30885  2ndresdju  30887  fsumiunle  31045  gsummpt2d  31211  cnre2csqima  31763  tpr2rico  31764  esum2dlem  31960  esumiun  31962  1stmbfm  32127  dya2iocnrect  32148  sibfof  32207  sitgaddlemb  32215  hgt750lemb  32536  satefvfmla0  33280  mvrsfpw  33368  msubff  33392  msubco  33393  msubvrs  33422  elxp8  35469  finixpnum  35689  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem31  35735  heicant  35739  mblfinlem1  35741  mblfinlem2  35742  ftc2nc  35786  heiborlem8  35903  dvhfvadd  39032  dvhvaddcl  39036  dvhvaddcomN  39037  dvhvaddass  39038  dvhvscacl  39044  dvhgrp  39048  dvhlveclem  39049  dibelval2nd  39093  dicelval2nd  39130  rmxypairf1o  40649  frmy  40652  cnmetcoval  42631  dvnprodlem1  43377  dvnprodlem2  43378  volicoff  43426  voliooicof  43427  etransclem44  43709  etransclem45  43710  etransclem47  43712  hoissre  43972  hoiprodcl  43975  ovnsubaddlem1  43998  ovnhoilem2  44030  hoicoto2  44033  ovncvr2  44039  opnvonmbllem2  44061  ovolval2lem  44071  ovolval3  44075  ovolval4lem1  44077  ovolval4lem2  44078  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085  smfpimbor1lem1  44219  2arymaptf  45886  rrx2xpref1o  45952