Theorem op2ndd 8023

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  Vcvv 3477  ⟨cop 4636  ‘cfv 6562  2^nd c2nd 8011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fv 6570  df-2nd 8013

This theorem is referenced by:  2nd2val  8041  xp2nd  8045  sbcopeq1a  8072  csbopeq1a  8073  eloprabi  8086  mpomptsx  8087  dmmpossx  8089  fmpox  8090  ovmptss  8116  fmpoco  8118  df2nd2  8122  frxp  8149  xporderlem  8150  fnwelem  8154  fimaproj  8158  xpord2lem  8165  naddcllem  8712  xpf1o  9177  mapunen  9184  xpwdomg  9622  hsmexlem2  10464  nqereu  10966  uzrdgfni  13995  fsumcom2  15806  fprodcom2  16016  qredeu  16691  comfeq  17750  isfuncd  17915  cofucl  17938  funcres2b  17947  funcpropd  17953  xpcco2nd  18240  xpccatid  18243  1stf2  18248  2ndf2  18251  1stfcl  18252  2ndfcl  18253  prf2fval  18256  prfcl  18258  evlf2  18274  evlfcl  18278  curf12  18283  curf1cl  18284  curf2  18285  curfcl  18288  hof2fval  18311  hofcl  18315  txbas  23590  cnmpt2nd  23692  txhmeo  23826  ptuncnv  23830  ptunhmeo  23831  xpstopnlem1  23832  xkohmeo  23838  prdstmdd  24147  ucnimalem  24304  fmucndlem  24315  fsum2cn  24908  ovoliunlem1  25550  2sqreuop  27520  2sqreuopnn  27521  2sqreuoplt  27522  2sqreuopltb  27523  2sqreuopnnlt  27524  2sqreuopnnltb  27525  noseqrdgfn  28326  wlkl0  30395  fcnvgreu  32689  fsumiunle  32835  gsummpt2co  33033  gsumhashmul  33046  gsumwrd2dccatlem  33051  gsumwrd2dccat  33052  elrgspnlem2  33232  esumiun  34074  eulerpartlemgs2  34361  hgt750lemb  34649  satfv1  35347  satefvfmla0  35402  msubrsub  35510  msubco  35515  msubvrs  35544  filnetlem4  36363  finixpnum  37591  poimirlem4  37610  poimirlem15  37621  poimirlem20  37626  poimirlem26  37632  heicant  37641  heiborlem4  37800  heiborlem6  37802  dicelvalN  41160  aks6d1c2p1  42099  aks6d1c3  42104  aks6d1c4  42105  aks6d1c6lem2  42152  aks6d1c6lem4  42154  aks6d1c7lem1  42161  fmpocos  42253  rmxypairf1o  42899  unxpwdom3  43083  fgraphxp  43192  elcnvlem  43590  dvnprodlem2  45902  etransclem46  46235  ovnsubaddlem1  46525  gpgvtxel2  47941  gpgvtx0  47943  gpgvtx1  47944  gpgedgvtx0  47953  gpgedgvtx1  47954  gpgvtxedg0  47955  gpgvtxedg1  47956  uspgrsprf  47989  uspgrsprf1  47990  dmmpossx2  48181  lmod1zr  48338  2arymaptf  48501  rrx2plordisom  48572  funcf2lem  48810