Theorem op2ndd 7997

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459  ⟨cop 4607  ‘cfv 6530  2^nd c2nd 7985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fv 6538  df-2nd 7987

This theorem is referenced by:  2nd2val  8015  xp2nd  8019  sbcopeq1a  8046  csbopeq1a  8047  eloprabi  8060  mpomptsx  8061  dmmpossx  8063  fmpox  8064  ovmptss  8090  fmpoco  8092  df2nd2  8096  frxp  8123  xporderlem  8124  fnwelem  8128  fimaproj  8132  xpord2lem  8139  naddcllem  8686  xpf1o  9151  mapunen  9158  xpwdomg  9597  hsmexlem2  10439  nqereu  10941  uzrdgfni  13974  fsumcom2  15788  fprodcom2  15998  qredeu  16675  comfeq  17716  isfuncd  17876  cofucl  17899  funcres2b  17908  funcpropd  17913  xpcco2nd  18195  xpccatid  18198  1stf2  18203  2ndf2  18206  1stfcl  18207  2ndfcl  18208  prf2fval  18211  prfcl  18213  evlf2  18228  evlfcl  18232  curf12  18237  curf1cl  18238  curf2  18239  curfcl  18242  hof2fval  18265  hofcl  18269  txbas  23503  cnmpt2nd  23605  txhmeo  23739  ptuncnv  23743  ptunhmeo  23744  xpstopnlem1  23745  xkohmeo  23751  prdstmdd  24060  ucnimalem  24216  fmucndlem  24227  fsum2cn  24811  ovoliunlem1  25453  2sqreuop  27423  2sqreuopnn  27424  2sqreuoplt  27425  2sqreuopltb  27426  2sqreuopnnlt  27427  2sqreuopnnltb  27428  noseqrdgfn  28229  wlkl0  30294  fcnvgreu  32597  fsumiunle  32754  gsummpt2co  32988  gsumhashmul  33001  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  elrgspnlem2  33184  elrgspnsubrunlem2  33189  esumiun  34071  eulerpartlemgs2  34358  hgt750lemb  34634  satfv1  35331  satefvfmla0  35386  msubrsub  35494  msubco  35499  msubvrs  35528  filnetlem4  36345  finixpnum  37575  poimirlem4  37594  poimirlem15  37605  poimirlem20  37610  poimirlem26  37616  heicant  37625  heiborlem4  37784  heiborlem6  37786  dicelvalN  41143  aks6d1c2p1  42077  aks6d1c3  42082  aks6d1c4  42083  aks6d1c6lem2  42130  aks6d1c6lem4  42132  aks6d1c7lem1  42139  fmpocos  42232  rmxypairf1o  42882  unxpwdom3  43066  fgraphxp  43175  elcnvlem  43572  dvnprodlem2  45924  etransclem46  46257  ovnsubaddlem1  46547  gpgvtxel2  48000  gpgvtx0  48005  gpgvtx1  48006  gpgedgvtx0  48013  gpgedgvtx1  48014  gpgvtxedg0  48015  gpgvtxedg1  48016  uspgrsprf  48069  uspgrsprf1  48070  dmmpossx2  48260  lmod1zr  48417  2arymaptf  48580  rrx2plordisom  48651  eloprab1st2nd  48791  funcf2lem  48994  tposcurf1  49158  reldmprcof2  49240  setc1ocofval  49327