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

Theorem op2ndd 7933
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 6843 . 2 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op2nd 7931 . 2 (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
51, 4eqtrdi 2793 1 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  Vcvv 3446  cop 4593  cfv 6497  2nd c2nd 7921
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fv 6505  df-2nd 7923
This theorem is referenced by:  2nd2val  7951  xp2nd  7955  sbcopeq1a  7982  csbopeq1a  7983  eloprabi  7996  mpomptsx  7997  dmmpossx  7999  fmpox  8000  ovmptss  8026  fmpoco  8028  df2nd2  8032  frxp  8059  xporderlem  8060  fnwelem  8064  fimaproj  8068  xpord2lem  8075  naddcllem  8623  xpf1o  9084  mapunen  9091  xpwdomg  9522  hsmexlem2  10364  nqereu  10866  uzrdgfni  13864  fsumcom2  15660  fprodcom2  15868  qredeu  16535  comfeq  17587  isfuncd  17752  cofucl  17775  funcres2b  17784  funcpropd  17788  xpcco2nd  18074  xpccatid  18077  1stf2  18082  2ndf2  18085  1stfcl  18086  2ndfcl  18087  prf2fval  18090  prfcl  18092  evlf2  18108  evlfcl  18112  curf12  18117  curf1cl  18118  curf2  18119  curfcl  18122  hof2fval  18145  hofcl  18149  txbas  22921  cnmpt2nd  23023  txhmeo  23157  ptuncnv  23161  ptunhmeo  23162  xpstopnlem1  23163  xkohmeo  23169  prdstmdd  23478  ucnimalem  23635  fmucndlem  23646  fsum2cn  24237  ovoliunlem1  24869  2sqreuop  26813  2sqreuopnn  26814  2sqreuoplt  26815  2sqreuopltb  26816  2sqreuopnnlt  26817  2sqreuopnnltb  26818  wlkl0  29314  fcnvgreu  31592  fsumiunle  31728  gsummpt2co  31893  gsumhashmul  31901  esumiun  32696  eulerpartlemgs2  32983  hgt750lemb  33272  satfv1  33960  satefvfmla0  34015  msubrsub  34123  msubco  34128  msubvrs  34157  filnetlem4  34856  finixpnum  36066  poimirlem4  36085  poimirlem15  36096  poimirlem20  36101  poimirlem26  36107  heicant  36116  heiborlem4  36276  heiborlem6  36278  dicelvalN  39644  aks6d1c2p1  40551  rmxypairf1o  41238  unxpwdom3  41425  fgraphxp  41541  elcnvlem  41880  dvnprodlem2  44195  etransclem46  44528  ovnsubaddlem1  44818  uspgrsprf  46055  uspgrsprf1  46056  dmmpossx2  46419  lmod1zr  46581  2arymaptf  46745  rrx2plordisom  46816  funcf2lem  47045
  Copyright terms: Public domain W3C validator