Theorem op2ndd 7988

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474  ⟨cop 4634  ‘cfv 6543  2^nd c2nd 7976

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fv 6551  df-2nd 7978

This theorem is referenced by:  2nd2val  8006  xp2nd  8010  sbcopeq1a  8037  csbopeq1a  8038  eloprabi  8051  mpomptsx  8052  dmmpossx  8054  fmpox  8055  ovmptss  8081  fmpoco  8083  df2nd2  8087  frxp  8114  xporderlem  8115  fnwelem  8119  fimaproj  8123  xpord2lem  8130  naddcllem  8677  xpf1o  9141  mapunen  9148  xpwdomg  9582  hsmexlem2  10424  nqereu  10926  uzrdgfni  13927  fsumcom2  15724  fprodcom2  15932  qredeu  16599  comfeq  17654  isfuncd  17819  cofucl  17842  funcres2b  17851  funcpropd  17855  xpcco2nd  18141  xpccatid  18144  1stf2  18149  2ndf2  18152  1stfcl  18153  2ndfcl  18154  prf2fval  18157  prfcl  18159  evlf2  18175  evlfcl  18179  curf12  18184  curf1cl  18185  curf2  18186  curfcl  18189  hof2fval  18212  hofcl  18216  txbas  23291  cnmpt2nd  23393  txhmeo  23527  ptuncnv  23531  ptunhmeo  23532  xpstopnlem1  23533  xkohmeo  23539  prdstmdd  23848  ucnimalem  24005  fmucndlem  24016  fsum2cn  24609  ovoliunlem1  25243  2sqreuop  27189  2sqreuopnn  27190  2sqreuoplt  27191  2sqreuopltb  27192  2sqreuopnnlt  27193  2sqreuopnnltb  27194  wlkl0  29875  fcnvgreu  32153  fsumiunle  32290  gsummpt2co  32458  gsumhashmul  32466  esumiun  33378  eulerpartlemgs2  33665  hgt750lemb  33954  satfv1  34640  satefvfmla0  34695  msubrsub  34803  msubco  34808  msubvrs  34837  filnetlem4  35569  finixpnum  36776  poimirlem4  36795  poimirlem15  36806  poimirlem20  36811  poimirlem26  36817  heicant  36826  heiborlem4  36985  heiborlem6  36987  dicelvalN  40352  aks6d1c2p1  41262  fmpocos  41362  rmxypairf1o  41952  unxpwdom3  42139  fgraphxp  42255  elcnvlem  42654  dvnprodlem2  44962  etransclem46  45295  ovnsubaddlem1  45585  uspgrsprf  46823  uspgrsprf1  46824  dmmpossx2  47101  lmod1zr  47262  2arymaptf  47426  rrx2plordisom  47497  funcf2lem  47726