Theorem op2ndd 7996

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  Vcvv 3453  ⟨cop 4594  ‘cfv 6536  2^nd c2nd 7984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fv 6544  df-2nd 7986

This theorem is referenced by:  2nd2val  8014  xp2nd  8018  sbcopeq1a  8045  csbopeq1a  8046  eloprabi  8059  mpomptsx  8060  dmmpossx  8062  fmpox  8063  ovmptss  8087  fmpoco  8089  df2nd2  8093  frxp  8121  xporderlem  8122  fnwelem  8126  fimaproj  8130  xpord2lem  8137  naddcllem  8661  xpf1o  9126  mapunen  9133  xpwdomg  9546  hsmexlem2  10410  nqereu  10913  uzrdgfni  13994  fsumcom2  15825  fprodcom2  16038  qredeu  16715  comfeq  17761  isfuncd  17921  cofucl  17944  funcres2b  17953  funcpropd  17958  xpcco2nd  18240  xpccatid  18243  1stf2  18248  2ndf2  18251  1stfcl  18252  2ndfcl  18253  prf2fval  18256  prfcl  18258  evlf2  18273  evlfcl  18277  curf12  18282  curf1cl  18283  curf2  18284  curfcl  18287  hof2fval  18310  hofcl  18314  txbas  23703  cnmpt2nd  23805  txhmeo  23939  ptuncnv  23943  ptunhmeo  23944  xpstopnlem1  23945  xkohmeo  23951  prdstmdd  24260  ucnimalem  24415  fmucndlem  24426  fsum2cn  25009  ovoliunlem1  25640  2sqreuop  27602  2sqreuopnn  27603  2sqreuoplt  27604  2sqreuopltb  27605  2sqreuopnnlt  27606  2sqreuopnnltb  27607  noseqrdgfn  28475  wlkl0  30684  fcnvgreu  32983  fsumiunle  33139  gsummpt2co  33334  gsumhashmul  33353  gsumwrd2dccatlem  33363  gsumwrd2dccat  33364  conjga  33456  elrgspnlem2  33529  elrgspnsubrunlem2  33534  mplvrpmga  33901  esumiun  34450  eulerpartlemgs2  34736  hgt750lemb  35009  satfv1  35821  satefvfmla0  35876  msubrsub  35984  msubco  35989  msubvrs  36018  nmulprop  36648  filnetlem4  36858  finixpnum  38222  poimirlem4  38241  poimirlem15  38252  poimirlem20  38257  poimirlem26  38263  heicant  38272  heiborlem4  38431  heiborlem6  38433  dicelvalN  41920  aks6d1c2p1  42853  aks6d1c3  42858  aks6d1c4  42859  aks6d1c6lem2  42906  aks6d1c6lem4  42908  aks6d1c7lem1  42915  fmpocos  42972  rmxypairf1o  43608  unxpwdom3  43792  fgraphxp  43901  elcnvlem  44297  dvnprodlem2  46631  etransclem46  46964  ovnsubaddlem1  47254  gpgvtxel2  48780  gpgvtx0  48785  gpgvtx1  48786  gpgedgvtx0  48793  gpgedgvtx1  48794  gpgvtxedg0  48795  gpgvtxedg1  48796  pgnbgreunbgrlem1  48845  pgnbgreunbgrlem2  48849  pgnbgreunbgrlem4  48851  pgnbgreunbgrlem5  48855  uspgrsprf  48878  uspgrsprf1  48879  dmmpossx2  49084  lmod1zr  49240  2arymaptf  49399  rrx2plordisom  49470  eloprab1st2nd  49613  funcf2lem  49826  oppf2  49885  tposcurf1  50044  reldmprcof2  50127  opf12  50149  setc1ocofval  50239