Theorem op2ndd 7944

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 6832	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = (2nd ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op2nd 7942	. 2 ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
5	1, 4	eqtrdi 2788	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ⟨cop 4574  ‘cfv 6490  2^nd c2nd 7932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fv 6498  df-2nd 7934

This theorem is referenced by:  2nd2val  7962  xp2nd  7966  sbcopeq1a  7993  csbopeq1a  7994  eloprabi  8007  mpomptsx  8008  dmmpossx  8010  fmpox  8011  ovmptss  8034  fmpoco  8036  df2nd2  8040  frxp  8067  xporderlem  8068  fnwelem  8072  fimaproj  8076  xpord2lem  8083  naddcllem  8603  xpf1o  9068  mapunen  9075  xpwdomg  9491  hsmexlem2  10338  nqereu  10841  uzrdgfni  13909  fsumcom2  15725  fprodcom2  15938  qredeu  16616  comfeq  17661  isfuncd  17821  cofucl  17844  funcres2b  17853  funcpropd  17858  xpcco2nd  18140  xpccatid  18143  1stf2  18148  2ndf2  18151  1stfcl  18152  2ndfcl  18153  prf2fval  18156  prfcl  18158  evlf2  18173  evlfcl  18177  curf12  18182  curf1cl  18183  curf2  18184  curfcl  18187  hof2fval  18210  hofcl  18214  txbas  23541  cnmpt2nd  23643  txhmeo  23777  ptuncnv  23781  ptunhmeo  23782  xpstopnlem1  23783  xkohmeo  23789  prdstmdd  24098  ucnimalem  24253  fmucndlem  24264  fsum2cn  24847  ovoliunlem1  25478  2sqreuop  27444  2sqreuopnn  27445  2sqreuoplt  27446  2sqreuopltb  27447  2sqreuopnnlt  27448  2sqreuopnnltb  27449  noseqrdgfn  28317  wlkl0  30457  fcnvgreu  32765  fsumiunle  32922  gsummpt2co  33129  gsumhashmul  33148  gsumwrd2dccatlem  33158  gsumwrd2dccat  33159  conjga  33251  elrgspnlem2  33324  elrgspnsubrunlem2  33329  mplvrpmga  33709  esumiun  34259  eulerpartlemgs2  34545  hgt750lemb  34821  satfv1  35566  satefvfmla0  35621  msubrsub  35729  msubco  35734  msubvrs  35763  filnetlem4  36584  finixpnum  37937  poimirlem4  37956  poimirlem15  37967  poimirlem20  37972  poimirlem26  37978  heicant  37987  heiborlem4  38146  heiborlem6  38148  dicelvalN  41635  aks6d1c2p1  42568  aks6d1c3  42573  aks6d1c4  42574  aks6d1c6lem2  42621  aks6d1c6lem4  42623  aks6d1c7lem1  42630  fmpocos  42686  rmxypairf1o  43354  unxpwdom3  43538  fgraphxp  43647  elcnvlem  44043  dvnprodlem2  46390  etransclem46  46723  ovnsubaddlem1  47013  gpgvtxel2  48521  gpgvtx0  48526  gpgvtx1  48527  gpgedgvtx0  48534  gpgedgvtx1  48535  gpgvtxedg0  48536  gpgvtxedg1  48537  pgnbgreunbgrlem1  48586  pgnbgreunbgrlem2  48590  pgnbgreunbgrlem4  48592  pgnbgreunbgrlem5  48596  uspgrsprf  48619  uspgrsprf1  48620  dmmpossx2  48810  lmod1zr  48966  2arymaptf  49125  rrx2plordisom  49196  eloprab1st2nd  49340  funcf2lem  49553  oppf2  49612  tposcurf1  49771  reldmprcof2  49854  opf12  49876  setc1ocofval  49966