Theorem op2ndd 7995

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3450  ⟨cop 4589  ‘cfv 6527  2^nd c2nd 7983

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-iota 6483  df-fun 6529  df-fv 6535  df-2nd 7985

This theorem is used by:  2nd2val  8013  xp2nd  8017  sbcopeq1a  8043  csbopeq1a  8044  eloprabi  8057  mpomptsx  8058  dmmpossx  8060  fmpox  8061  ovmptss  8087  fmpoco  8089  df2nd2  8093  frxp  8121  xporderlem  8122  fnwelem  8126  fimaproj  8130  xpord2lem  8137  naddcllem  8663  xpf1o  9136  mapunen  9143  xpwdomg  9557  hsmexlem2  10477  nqereu  10986  uzrdgfni  14070  fsumcom2  15908  fprodcom2  16119  qredeu  16796  comfeq  17842  isfuncd  18002  cofucl  18025  funcres2b  18034  funcpropd  18039  xpcco2nd  18321  xpccatid  18324  1stf2  18329  2ndf2  18332  1stfcl  18333  2ndfcl  18334  prf2fval  18337  prfcl  18339  evlf2  18354  evlfcl  18358  curf12  18363  curf1cl  18364  curf2  18365  curfcl  18368  hof2fval  18391  hofcl  18395  txbas  23848  cnmpt2nd  23950  txhmeo  24084  ptuncnv  24088  ptunhmeo  24089  xpstopnlem1  24090  xkohmeo  24096  prdstmdd  24405  ucnimalem  24560  fmucndlem  24571  fsum2cn  25154  ovoliunlem1  25785  2sqreuop  27753  2sqreuopnn  27754  2sqreuoplt  27755  2sqreuopltb  27756  2sqreuopnnlt  27757  2sqreuopnnltb  27758  noseqrdgfn  28626  wlkl0  30902  fcnvgreu  33200  fsumiunle  33354  gsummpt2co  33543  gsumhashmul  33562  gsumwrd2dccatlem  33572  gsumwrd2dccat  33573  conjga  33665  elrgspnlem2  33738  elrgspnsubrunlem2  33743  mplvrpmga  34111  esumiun  34660  eulerpartlemgs2  34947  hgt750lemb  35220  satfv1  36049  satefvfmla0  36104  msubrsub  36212  msubco  36217  msubvrs  36246  nmulprop  36861  filnetlem4  37091  finixpnum  38448  poimirlem4  38462  poimirlem15  38473  poimirlem20  38478  poimirlem26  38484  heicant  38493  heiborlem4  38668  heiborlem6  38670  dicelvalN  42155  aks6d1c2p1  43088  aks6d1c3  43093  aks6d1c4  43094  aks6d1c6lem2  43141  aks6d1c6lem4  43143  aks6d1c7lem1  43150  fmpocos  43207  rmxypairf1o  43856  unxpwdom3  44040  fgraphxp  44149  elcnvlem  44545  dvnprodlem2  46879  etransclem46  47212  ovnsubaddlem1  47502  gpgvtxel2  49068  gpgvtx0  49073  gpgvtx1  49074  gpgedgvtx0  49081  gpgedgvtx1  49082  gpgvtxedg0  49083  gpgvtxedg1  49084  pgnbgreunbgrlem1  49133  pgnbgreunbgrlem2  49137  pgnbgreunbgrlem4  49139  pgnbgreunbgrlem5  49143  uspgrsprf  49166  uspgrsprf1  49167  dmmpossx2  49371  lmod1zr  49527  2arymaptf  49686  rrx2plordisom  49757  eloprab1st2nd  49900  funcf2lem  50111  oppf2  50170  tposcurf1  50329  reldmprcof2  50412  opf12  50434  setc1ocofval  50524