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

Theorem op2ndd 7070
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 6103 . 2 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op2nd 7068 . 2 (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
51, 4syl6eq 2660 1 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  Vcvv 3173  cop 4131  cfv 5804  2nd c2nd 7058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fv 5812  df-2nd 7060
This theorem is referenced by:  2nd2val  7086  xp2nd  7090  sbcopeq1a  7111  csbopeq1a  7112  eloprabi  7121  mpt2mptsx  7122  dmmpt2ssx  7124  fmpt2x  7125  ovmptss  7145  fmpt2co  7147  df2nd2  7151  frxp  7174  xporderlem  7175  fnwelem  7179  xpf1o  8007  mapunen  8014  xpwdomg  8373  hsmexlem2  9132  nqereu  9630  uzrdgfni  12619  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  qredeu  15210  comfeq  16189  isfuncd  16348  cofucl  16371  funcres2b  16380  funcpropd  16383  xpcco2nd  16648  xpccatid  16651  1stf2  16656  2ndf2  16659  1stfcl  16660  2ndfcl  16661  prf2fval  16664  prfcl  16666  evlf2  16681  evlfcl  16685  curf12  16690  curf1cl  16691  curf2  16692  curfcl  16695  hof2fval  16718  hofcl  16722  txbas  21180  cnmpt2nd  21282  txhmeo  21416  ptuncnv  21420  ptunhmeo  21421  xpstopnlem1  21422  xkohmeo  21428  prdstmdd  21737  ucnimalem  21894  fmucndlem  21905  fsum2cn  22482  ovoliunlem1  23077  usgrac  25880  edgss  25881  fcnvgreu  28855  gsummpt2co  29111  fimaproj  29228  esumiun  29483  eulerpartlemgs2  29769  msubrsub  30677  msubco  30682  msubvrs  30711  filnetlem4  31546  finixpnum  32564  poimirlem4  32583  poimirlem15  32594  poimirlem20  32599  poimirlem26  32605  heicant  32614  heiborlem4  32783  heiborlem6  32785  dicelvalN  35485  rmxypairf1o  36494  unxpwdom3  36683  fgraphxp  36808  elcnvlem  36926  dvnprodlem2  38837  etransclem46  39173  ovnsubaddlem1  39460  dmmpt2ssx2  41908  lmod1zr  42076
  Copyright terms: Public domain W3C validator