Theorem op2ndd 8036

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

Step	Hyp	Ref	Expression
1		fveq2 6908	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op2nd 8034	. 2 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
5	1, 4	eqtrdi 2814	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ⟨cop 4838  ‘cfv 6558  2^nd c2nd 8024

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fv 6566  df-2nd 8026

This theorem is used by:  2nd2val  8054  xp2nd  8058  sbcopeq1a  8085  csbopeq1a  8086  eloprabi  8099  mpomptsx  8100  dmmpossx  8102  fmpox  8103  ovmptssOLD  8130  fmpoco  8132  df2nd2  8137  frxp  8165  xporderlem  8166  fnwelem  8170  fimaproj  8179  xpord2lem  8186  naddcllem  8713  xpf1o  9186  mapunen  9193  xpwdomg  9606  hsmexlem2  10532  nqereu  11041  uzrdgfni  14128  fsumcom2  15969  fprodcom2  16180  qredeu  16862  comfeq  17909  isfuncd  18069  cofucl  18092  funcres2b  18101  funcpropd  18106  xpcco2nd  18388  xpccatid  18391  1stf2  18396  2ndf2  18399  1stfcl  18400  2ndfcl  18401  prf2fval  18404  prfcl  18406  evlf2  18421  evlfcl  18425  curf12  18430  curf1cl  18431  curf2  18432  curfcl  18435  hof2fval  18458  hofcl  18462  txbas  23916  cnmpt2nd  24018  txhmeo  24152  ptuncnv  24156  ptunhmeo  24157  xpstopnlem1  24158  xkohmeo  24164  prdstmdd  24473  ucnimalem  24628  fmucndlem  24639  fsum2cn  25222  ovoliunlem1  25853  2sqreuop  27819  2sqreuopnn  27820  2sqreuoplt  27821  2sqreuopltb  27822  2sqreuopnnlt  27823  2sqreuopnnltb  27824  noseqrdgfn  28722  wlkl0  30998  fcnvgreu  33338  fsumiunle  33490  gsummpt2co  33679  gsumhashmul  33698  gsumwrd2dccatlem  33708  gsumwrd2dccat  33709  conjga  33801  elrgspnlem2  33874  elrgspnsubrunlem2  33879  mplvrpmga  34247  esumiun  34796  eulerpartlemgs2  35082  hgt750lemb  35355  dfj2  36009  jf1o  36011  satfv1  36295  satefvfmla0  36350  msubrsub  36458  msubco  36463  msubvrs  36492  nmulprop  37117  filnetlem4  37347  finixpnum  38720  poimirlem4  38734  poimirlem15  38745  poimirlem20  38750  poimirlem26  38756  heicant  38765  heiborlem4  38940  heiborlem6  38942  dicelvalN  42427  aks6d1c2p1  43360  aks6d1c3  43365  aks6d1c4  43366  aks6d1c6lem2  43413  aks6d1c6lem4  43415  aks6d1c7lem1  43422  fmpocos  43480  rmxypairf1o  44111  unxpwdom3  44290  fgraphxp  44398  elcnvlem  44793  dvnprodlem2  47162  etransclem46  47495  ovnsubaddlem1  47785  gpgvtxel2  49351  gpgvtx0  49356  gpgvtx1  49357  gpgedgvtx0  49364  gpgedgvtx1  49365  gpgvtxedg0  49366  gpgvtxedg1  49367  pgnbgreunbgrlem1  49416  pgnbgreunbgrlem2  49420  pgnbgreunbgrlem4  49422  pgnbgreunbgrlem5  49426  uspgrsprf  49449  uspgrsprf1  49450  dmmpossx2  49654  lmod1zr  49810  2arymaptf  49969  rrx2plordisom  50041  eloprab1st2nd  50184  funcf2lem  50400  oppf2  50461  tposcurf1  50626  postcof2nd  50704  reldmprcof2  50722  opf12  50744  setc1ocofval  50834  fuconuniqlem  50986  fuconuniqvalslem  50988