Theorem op2ndd 7981

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ⟨cop 4633  ‘cfv 6540  2^nd c2nd 7969

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 5298  ax-nul 5305  ax-pr 5426  ax-un 7720

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 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6492  df-fun 6542  df-fv 6548  df-2nd 7971

This theorem is referenced by:  2nd2val  7999  xp2nd  8003  sbcopeq1a  8030  csbopeq1a  8031  eloprabi  8044  mpomptsx  8045  dmmpossx  8047  fmpox  8048  ovmptss  8074  fmpoco  8076  df2nd2  8080  frxp  8107  xporderlem  8108  fnwelem  8112  fimaproj  8116  xpord2lem  8123  naddcllem  8671  xpf1o  9135  mapunen  9142  xpwdomg  9576  hsmexlem2  10418  nqereu  10920  uzrdgfni  13919  fsumcom2  15716  fprodcom2  15924  qredeu  16591  comfeq  17646  isfuncd  17811  cofucl  17834  funcres2b  17843  funcpropd  17847  xpcco2nd  18133  xpccatid  18136  1stf2  18141  2ndf2  18144  1stfcl  18145  2ndfcl  18146  prf2fval  18149  prfcl  18151  evlf2  18167  evlfcl  18171  curf12  18176  curf1cl  18177  curf2  18178  curfcl  18181  hof2fval  18204  hofcl  18208  txbas  23053  cnmpt2nd  23155  txhmeo  23289  ptuncnv  23293  ptunhmeo  23294  xpstopnlem1  23295  xkohmeo  23301  prdstmdd  23610  ucnimalem  23767  fmucndlem  23778  fsum2cn  24369  ovoliunlem1  25001  2sqreuop  26945  2sqreuopnn  26946  2sqreuoplt  26947  2sqreuopltb  26948  2sqreuopnnlt  26949  2sqreuopnnltb  26950  wlkl0  29600  fcnvgreu  31876  fsumiunle  32013  gsummpt2co  32178  gsumhashmul  32186  esumiun  33030  eulerpartlemgs2  33317  hgt750lemb  33606  satfv1  34292  satefvfmla0  34347  msubrsub  34455  msubco  34460  msubvrs  34489  filnetlem4  35204  finixpnum  36411  poimirlem4  36430  poimirlem15  36441  poimirlem20  36446  poimirlem26  36452  heicant  36461  heiborlem4  36620  heiborlem6  36622  dicelvalN  39987  aks6d1c2p1  40894  fmpocos  41005  rmxypairf1o  41583  unxpwdom3  41770  fgraphxp  41886  elcnvlem  42285  dvnprodlem2  44598  etransclem46  44931  ovnsubaddlem1  45221  uspgrsprf  46459  uspgrsprf1  46460  dmmpossx2  46914  lmod1zr  47076  2arymaptf  47240  rrx2plordisom  47311  funcf2lem  47540