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

Theorem op2ndd 7377
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 6375 . 2 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op2nd 7375 . 2 (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
51, 4syl6eq 2815 1 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wcel 2155  Vcvv 3350  cop 4340  cfv 6068  2nd c2nd 7365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-iota 6031  df-fun 6070  df-fv 6076  df-2nd 7367
This theorem is referenced by:  2nd2val  7395  xp2nd  7399  sbcopeq1a  7420  csbopeq1a  7421  eloprabi  7433  mpt2mptsx  7434  dmmpt2ssx  7436  fmpt2x  7437  ovmptss  7460  fmpt2co  7462  df2nd2  7466  frxp  7489  xporderlem  7490  fnwelem  7494  xpf1o  8329  mapunen  8336  xpwdomg  8697  hsmexlem2  9502  nqereu  10004  uzrdgfni  12965  fsumcom2  14790  fprodcom2  14997  qredeu  15652  comfeq  16631  isfuncd  16790  cofucl  16813  funcres2b  16822  funcpropd  16825  xpcco2nd  17091  xpccatid  17094  1stf2  17099  2ndf2  17102  1stfcl  17103  2ndfcl  17104  prf2fval  17107  prfcl  17109  evlf2  17124  evlfcl  17128  curf12  17133  curf1cl  17134  curf2  17135  curfcl  17138  hof2fval  17161  hofcl  17165  txbas  21650  cnmpt2nd  21752  txhmeo  21886  ptuncnv  21890  ptunhmeo  21891  xpstopnlem1  21892  xkohmeo  21898  prdstmdd  22206  ucnimalem  22363  fmucndlem  22374  fsum2cn  22953  ovoliunlem1  23560  wlkl0  27671  fcnvgreu  29921  fsumiunle  30024  gsummpt2co  30227  fimaproj  30347  esumiun  30603  eulerpartlemgs2  30889  hgt750lemb  31185  msubrsub  31871  msubco  31876  msubvrs  31905  filnetlem4  32819  finixpnum  33818  poimirlem4  33837  poimirlem15  33848  poimirlem20  33853  poimirlem26  33859  heicant  33868  heiborlem4  34035  heiborlem6  34037  dicelvalN  37134  rmxypairf1o  38153  unxpwdom3  38342  fgraphxp  38466  elcnvlem  38582  dvnprodlem2  40800  etransclem46  41134  ovnsubaddlem1  41424  uspgrsprf  42423  uspgrsprf1  42424  dmmpt2ssx2  42784  lmod1zr  42951
  Copyright terms: Public domain W3C validator