Theorem op2ndd 7946

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3441  ⟨cop 4587  ‘cfv 6493  2^nd c2nd 7934

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 5242  ax-nul 5252  ax-pr 5378  ax-un 7682

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fv 6501  df-2nd 7936

This theorem is referenced by:  2nd2val  7964  xp2nd  7968  sbcopeq1a  7995  csbopeq1a  7996  eloprabi  8009  mpomptsx  8010  dmmpossx  8012  fmpox  8013  ovmptss  8037  fmpoco  8039  df2nd2  8043  frxp  8070  xporderlem  8071  fnwelem  8075  fimaproj  8079  xpord2lem  8086  naddcllem  8606  xpf1o  9071  mapunen  9078  xpwdomg  9494  hsmexlem2  10341  nqereu  10844  uzrdgfni  13885  fsumcom2  15701  fprodcom2  15911  qredeu  16589  comfeq  17633  isfuncd  17793  cofucl  17816  funcres2b  17825  funcpropd  17830  xpcco2nd  18112  xpccatid  18115  1stf2  18120  2ndf2  18123  1stfcl  18124  2ndfcl  18125  prf2fval  18128  prfcl  18130  evlf2  18145  evlfcl  18149  curf12  18154  curf1cl  18155  curf2  18156  curfcl  18159  hof2fval  18182  hofcl  18186  txbas  23515  cnmpt2nd  23617  txhmeo  23751  ptuncnv  23755  ptunhmeo  23756  xpstopnlem1  23757  xkohmeo  23763  prdstmdd  24072  ucnimalem  24227  fmucndlem  24238  fsum2cn  24822  ovoliunlem1  25463  2sqreuop  27433  2sqreuopnn  27434  2sqreuoplt  27435  2sqreuopltb  27436  2sqreuopnnlt  27437  2sqreuopnnltb  27438  noseqrdgfn  28287  wlkl0  30425  fcnvgreu  32732  fsumiunle  32891  gsummpt2co  33112  gsumhashmul  33131  gsumwrd2dccatlem  33140  gsumwrd2dccat  33141  conjga  33233  elrgspnlem2  33306  elrgspnsubrunlem2  33311  mplvrpmga  33691  esumiun  34232  eulerpartlemgs2  34518  hgt750lemb  34794  satfv1  35538  satefvfmla0  35593  msubrsub  35701  msubco  35706  msubvrs  35735  filnetlem4  36556  finixpnum  37777  poimirlem4  37796  poimirlem15  37807  poimirlem20  37812  poimirlem26  37818  heicant  37827  heiborlem4  37986  heiborlem6  37988  dicelvalN  41475  aks6d1c2p1  42409  aks6d1c3  42414  aks6d1c4  42415  aks6d1c6lem2  42462  aks6d1c6lem4  42464  aks6d1c7lem1  42471  fmpocos  42527  rmxypairf1o  43189  unxpwdom3  43373  fgraphxp  43482  elcnvlem  43878  dvnprodlem2  46227  etransclem46  46560  ovnsubaddlem1  46850  gpgvtxel2  48330  gpgvtx0  48335  gpgvtx1  48336  gpgedgvtx0  48343  gpgedgvtx1  48344  gpgvtxedg0  48345  gpgvtxedg1  48346  pgnbgreunbgrlem1  48395  pgnbgreunbgrlem2  48399  pgnbgreunbgrlem4  48401  pgnbgreunbgrlem5  48405  uspgrsprf  48428  uspgrsprf1  48429  dmmpossx2  48619  lmod1zr  48775  2arymaptf  48934  rrx2plordisom  49005  eloprab1st2nd  49149  funcf2lem  49362  oppf2  49421  tposcurf1  49580  reldmprcof2  49663  opf12  49685  setc1ocofval  49775