MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  op2ndd Structured version   Unicode version

Theorem op2ndd 6588
Description: Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
op1st.1  |-  A  e. 
_V
op1st.2  |-  B  e. 
_V
Assertion
Ref Expression
op2ndd  |-  ( C  =  <. A ,  B >.  ->  ( 2nd `  C
)  =  B )

Proof of Theorem op2ndd
StepHypRef Expression
1 fveq2 5691 . 2  |-  ( C  =  <. A ,  B >.  ->  ( 2nd `  C
)  =  ( 2nd `  <. A ,  B >. ) )
2 op1st.1 . . 3  |-  A  e. 
_V
3 op1st.2 . . 3  |-  B  e. 
_V
42, 3op2nd 6586 . 2  |-  ( 2nd `  <. A ,  B >. )  =  B
51, 4syl6eq 2491 1  |-  ( C  =  <. A ,  B >.  ->  ( 2nd `  C
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   _Vcvv 2972   <.cop 3883   ` cfv 5418   2ndc2nd 6576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-iota 5381  df-fun 5420  df-fv 5426  df-2nd 6578
This theorem is referenced by:  2nd2val  6603  xp2nd  6607  sbcopeq1a  6626  csbopeq1a  6627  eloprabi  6636  mpt2mptsx  6637  dmmpt2ssx  6639  fmpt2x  6640  ovmptss  6654  fmpt2co  6656  df2nd2  6660  frxp  6682  xporderlem  6683  fnwelem  6687  xpf1o  7473  mapunen  7480  xpwdomg  7800  hsmexlem2  8596  nqereu  9098  uzrdgfni  11781  fsumcom2  13241  qredeu  13793  comfeq  14645  isfuncd  14775  cofucl  14798  funcres2b  14807  funcpropd  14810  xpcco2nd  14995  xpccatid  14998  1stf2  15003  2ndf2  15006  1stfcl  15007  2ndfcl  15008  prf2fval  15011  prfcl  15013  evlf2  15028  evlfcl  15032  curf12  15037  curf1cl  15038  curf2  15039  curfcl  15042  hof2fval  15065  hofcl  15069  txbas  19140  cnmpt2nd  19242  txhmeo  19376  ptuncnv  19380  ptunhmeo  19381  xpstopnlem1  19382  xkohmeo  19388  prdstmdd  19694  ucnimalem  19855  fmucndlem  19866  fsum2cn  20447  ovoliunlem1  20985  fcnvgreu  25991  gsummpt2co  26249  eulerpartlemgs2  26763  fprodcom2  27495  finixpnum  28414  heicant  28426  filnetlem4  28602  heiborlem4  28713  heiborlem6  28715  rmxypairf1o  29252  unxpwdom3  29448  fgraphxp  29579  dmmpt2ssx2  30727  lmod1zr  31035  dicelvalN  34823
  Copyright terms: Public domain W3C validator