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

Theorem op2ndd 7694
Description: Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
op1st.1 𝐴 ∈ V
op1st.2 𝐵 ∈ V
Assertion
Ref Expression
op2ndd (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = 𝐵)

Proof of Theorem op2ndd
StepHypRef Expression
1 fveq2 6666 . 2 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op2nd 7692 . 2 (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
51, 4syl6eq 2876 1 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2106  Vcvv 3499  cop 4569  cfv 6351  2nd c2nd 7682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-iota 6311  df-fun 6353  df-fv 6359  df-2nd 7684
This theorem is referenced by:  2nd2val  7712  xp2nd  7716  sbcopeq1a  7742  csbopeq1a  7743  eloprabi  7755  mpomptsx  7756  dmmpossx  7758  fmpox  7759  ovmptss  7782  fmpoco  7784  df2nd2  7788  frxp  7814  xporderlem  7815  fnwelem  7819  fimaproj  7823  xpf1o  8671  mapunen  8678  xpwdomg  9041  hsmexlem2  9841  nqereu  10343  uzrdgfni  13319  fsumcom2  15121  fprodcom2  15330  qredeu  15994  comfeq  16968  isfuncd  17127  cofucl  17150  funcres2b  17159  funcpropd  17162  xpcco2nd  17427  xpccatid  17430  1stf2  17435  2ndf2  17438  1stfcl  17439  2ndfcl  17440  prf2fval  17443  prfcl  17445  evlf2  17460  evlfcl  17464  curf12  17469  curf1cl  17470  curf2  17471  curfcl  17474  hof2fval  17497  hofcl  17501  txbas  22091  cnmpt2nd  22193  txhmeo  22327  ptuncnv  22331  ptunhmeo  22332  xpstopnlem1  22333  xkohmeo  22339  prdstmdd  22647  ucnimalem  22804  fmucndlem  22815  fsum2cn  23394  ovoliunlem1  24018  2sqreuop  25952  2sqreuopnn  25953  2sqreuoplt  25954  2sqreuopltb  25955  2sqreuopnnlt  25956  2sqreuopnnltb  25957  wlkl0  28061  fcnvgreu  30334  fsumiunle  30460  gsummpt2co  30601  esumiun  31240  eulerpartlemgs2  31525  hgt750lemb  31814  satfv1  32495  satefvfmla0  32550  msubrsub  32658  msubco  32663  msubvrs  32692  filnetlem4  33614  finixpnum  34745  poimirlem4  34764  poimirlem15  34775  poimirlem20  34780  poimirlem26  34786  heicant  34795  heiborlem4  34961  heiborlem6  34963  dicelvalN  38182  rmxypairf1o  39370  unxpwdom3  39557  fgraphxp  39673  elcnvlem  39823  dvnprodlem2  42094  etransclem46  42428  ovnsubaddlem1  42715  uspgrsprf  43850  uspgrsprf1  43851  dmmpossx2  44214  lmod1zr  44377  rrx2plordisom  44539
  Copyright terms: Public domain W3C validator