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

Theorem op2ndd 7047
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 6087 . 2 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op2nd 7045 . 2 (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
51, 4syl6eq 2659 1 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  Vcvv 3172  cop 4130  cfv 5789  2nd c2nd 7035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-iota 5753  df-fun 5791  df-fv 5797  df-2nd 7037
This theorem is referenced by:  2nd2val  7063  xp2nd  7067  sbcopeq1a  7088  csbopeq1a  7089  eloprabi  7098  mpt2mptsx  7099  dmmpt2ssx  7101  fmpt2x  7102  ovmptss  7122  fmpt2co  7124  df2nd2  7128  frxp  7151  xporderlem  7152  fnwelem  7156  xpf1o  7984  mapunen  7991  xpwdomg  8350  hsmexlem2  9109  nqereu  9607  uzrdgfni  12576  fsumcom2  14295  fsumcom2OLD  14296  fprodcom2  14501  fprodcom2OLD  14502  qredeu  15158  comfeq  16137  isfuncd  16296  cofucl  16319  funcres2b  16328  funcpropd  16331  xpcco2nd  16596  xpccatid  16599  1stf2  16604  2ndf2  16607  1stfcl  16608  2ndfcl  16609  prf2fval  16612  prfcl  16614  evlf2  16629  evlfcl  16633  curf12  16638  curf1cl  16639  curf2  16640  curfcl  16643  hof2fval  16666  hofcl  16670  txbas  21127  cnmpt2nd  21229  txhmeo  21363  ptuncnv  21367  ptunhmeo  21368  xpstopnlem1  21369  xkohmeo  21375  prdstmdd  21684  ucnimalem  21841  fmucndlem  21852  fsum2cn  22429  ovoliunlem1  23021  usgrac  25673  edgss  25674  fcnvgreu  28648  gsummpt2co  28904  fimaproj  29021  esumiun  29276  eulerpartlemgs2  29562  msubrsub  30470  msubco  30475  msubvrs  30504  filnetlem4  31339  finixpnum  32347  poimirlem4  32366  poimirlem15  32377  poimirlem20  32382  poimirlem26  32388  heicant  32397  heiborlem4  32566  heiborlem6  32568  dicelvalN  35268  rmxypairf1o  36277  unxpwdom3  36466  fgraphxp  36591  elcnvlem  36709  dvnprodlem2  38620  etransclem46  38956  ovnsubaddlem1  39243  dmmpt2ssx2  41889  lmod1zr  42057
  Copyright terms: Public domain W3C validator