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

Theorem op2ndd 7347
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 6348 . 2 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2 op1st.1 . . 3 𝐴 ∈ V
3 op1st.2 . . 3 𝐵 ∈ V
42, 3op2nd 7345 . 2 (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
51, 4syl6eq 2824 1 (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1634  wcel 2148  Vcvv 3355  cop 4332  cfv 6042  2nd c2nd 7335
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3357  df-sbc 3594  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-mpt 4877  df-id 5171  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-iota 6005  df-fun 6044  df-fv 6050  df-2nd 7337
This theorem is referenced by:  2nd2val  7365  xp2nd  7369  sbcopeq1a  7390  csbopeq1a  7391  eloprabi  7403  mpt2mptsx  7404  dmmpt2ssx  7406  fmpt2x  7407  ovmptss  7430  fmpt2co  7432  df2nd2  7436  frxp  7459  xporderlem  7460  fnwelem  7464  xpf1o  8299  mapunen  8306  xpwdomg  8667  hsmexlem2  9472  nqereu  9974  uzrdgfni  12987  fsumcom2  14735  fprodcom2  14943  qredeu  15600  comfeq  16593  isfuncd  16752  cofucl  16775  funcres2b  16784  funcpropd  16787  xpcco2nd  17053  xpccatid  17056  1stf2  17061  2ndf2  17064  1stfcl  17065  2ndfcl  17066  prf2fval  17069  prfcl  17071  evlf2  17086  evlfcl  17090  curf12  17095  curf1cl  17096  curf2  17097  curfcl  17100  hof2fval  17123  hofcl  17127  txbas  21611  cnmpt2nd  21713  txhmeo  21847  ptuncnv  21851  ptunhmeo  21852  xpstopnlem1  21853  xkohmeo  21859  prdstmdd  22167  ucnimalem  22324  fmucndlem  22335  fsum2cn  22914  ovoliunlem1  23510  wlkl0  27575  fcnvgreu  29829  fsumiunle  29932  gsummpt2co  30137  fimaproj  30257  esumiun  30513  eulerpartlemgs2  30799  hgt750lemb  31091  msubrsub  31778  msubco  31783  msubvrs  31812  filnetlem4  32730  finixpnum  33744  poimirlem4  33763  poimirlem15  33774  poimirlem20  33779  poimirlem26  33785  heicant  33794  heiborlem4  33961  heiborlem6  33963  dicelvalN  37003  rmxypairf1o  38017  unxpwdom3  38206  fgraphxp  38330  elcnvlem  38447  dvnprodlem2  40686  etransclem46  41020  ovnsubaddlem1  41310  uspgrsprf  42306  uspgrsprf1  42307  dmmpt2ssx2  42667  lmod1zr  42834
  Copyright terms: Public domain W3C validator