Theorem op2ndd 7986

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ⟨cop 4635  ‘cfv 6544  2^nd c2nd 7974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fv 6552  df-2nd 7976

This theorem is referenced by:  2nd2val  8004  xp2nd  8008  sbcopeq1a  8035  csbopeq1a  8036  eloprabi  8049  mpomptsx  8050  dmmpossx  8052  fmpox  8053  ovmptss  8079  fmpoco  8081  df2nd2  8085  frxp  8112  xporderlem  8113  fnwelem  8117  fimaproj  8121  xpord2lem  8128  naddcllem  8675  xpf1o  9139  mapunen  9146  xpwdomg  9580  hsmexlem2  10422  nqereu  10924  uzrdgfni  13923  fsumcom2  15720  fprodcom2  15928  qredeu  16595  comfeq  17650  isfuncd  17815  cofucl  17838  funcres2b  17847  funcpropd  17851  xpcco2nd  18137  xpccatid  18140  1stf2  18145  2ndf2  18148  1stfcl  18149  2ndfcl  18150  prf2fval  18153  prfcl  18155  evlf2  18171  evlfcl  18175  curf12  18180  curf1cl  18181  curf2  18182  curfcl  18185  hof2fval  18208  hofcl  18212  txbas  23071  cnmpt2nd  23173  txhmeo  23307  ptuncnv  23311  ptunhmeo  23312  xpstopnlem1  23313  xkohmeo  23319  prdstmdd  23628  ucnimalem  23785  fmucndlem  23796  fsum2cn  24387  ovoliunlem1  25019  2sqreuop  26965  2sqreuopnn  26966  2sqreuoplt  26967  2sqreuopltb  26968  2sqreuopnnlt  26969  2sqreuopnnltb  26970  wlkl0  29651  fcnvgreu  31929  fsumiunle  32066  gsummpt2co  32231  gsumhashmul  32239  esumiun  33123  eulerpartlemgs2  33410  hgt750lemb  33699  satfv1  34385  satefvfmla0  34440  msubrsub  34548  msubco  34553  msubvrs  34582  filnetlem4  35314  finixpnum  36521  poimirlem4  36540  poimirlem15  36551  poimirlem20  36556  poimirlem26  36562  heicant  36571  heiborlem4  36730  heiborlem6  36732  dicelvalN  40097  aks6d1c2p1  41004  fmpocos  41104  rmxypairf1o  41698  unxpwdom3  41885  fgraphxp  42001  elcnvlem  42400  dvnprodlem2  44711  etransclem46  45044  ovnsubaddlem1  45334  uspgrsprf  46572  uspgrsprf1  46573  dmmpossx2  47060  lmod1zr  47222  2arymaptf  47386  rrx2plordisom  47457  funcf2lem  47686