Theorem op2ndd 7970

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

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  Vcvv 3448  ⟨cop 4582  ‘cfv 6510  2^nd c2nd 7958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pr 5384  ax-un 7707

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-iota 6466  df-fun 6512  df-fv 6518  df-2nd 7960

This theorem is referenced by:  2nd2val  7988  xp2nd  7992  sbcopeq1a  8019  csbopeq1a  8020  eloprabi  8033  mpomptsx  8034  dmmpossx  8036  fmpox  8037  ovmptss  8060  fmpoco  8062  df2nd2  8066  frxp  8094  xporderlem  8095  fnwelem  8099  fimaproj  8103  xpord2lem  8110  naddcllem  8634  xpf1o  9100  mapunen  9107  xpwdomg  9523  hsmexlem2  10374  nqereu  10877  uzrdgfni  13961  fsumcom2  15777  fprodcom2  15990  qredeu  16668  comfeq  17714  isfuncd  17874  cofucl  17897  funcres2b  17906  funcpropd  17911  xpcco2nd  18193  xpccatid  18196  1stf2  18201  2ndf2  18204  1stfcl  18205  2ndfcl  18206  prf2fval  18209  prfcl  18211  evlf2  18226  evlfcl  18230  curf12  18235  curf1cl  18236  curf2  18237  curfcl  18240  hof2fval  18263  hofcl  18267  txbas  23600  cnmpt2nd  23702  txhmeo  23836  ptuncnv  23840  ptunhmeo  23841  xpstopnlem1  23842  xkohmeo  23848  prdstmdd  24157  ucnimalem  24312  fmucndlem  24323  fsum2cn  24906  ovoliunlem1  25537  2sqreuop  27496  2sqreuopnn  27497  2sqreuoplt  27498  2sqreuopltb  27499  2sqreuopnnlt  27500  2sqreuopnnltb  27501  noseqrdgfn  28369  wlkl0  30508  fcnvgreu  32817  fsumiunle  32974  gsummpt2co  33182  gsumhashmul  33201  gsumwrd2dccatlem  33211  gsumwrd2dccat  33212  conjga  33304  elrgspnlem2  33378  elrgspnsubrunlem2  33383  mplvrpmga  33796  esumiun  34345  eulerpartlemgs2  34631  hgt750lemb  34907  satfv1  35661  satefvfmla0  35716  msubrsub  35824  msubco  35829  msubvrs  35858  nmulprop  36488  filnetlem4  36689  finixpnum  38052  poimirlem4  38071  poimirlem15  38082  poimirlem20  38087  poimirlem26  38093  heicant  38102  heiborlem4  38261  heiborlem6  38263  dicelvalN  41750  aks6d1c2p1  42683  aks6d1c3  42688  aks6d1c4  42689  aks6d1c6lem2  42736  aks6d1c6lem4  42738  aks6d1c7lem1  42745  fmpocos  42800  rmxypairf1o  43436  unxpwdom3  43620  fgraphxp  43729  elcnvlem  44125  dvnprodlem2  46469  etransclem46  46802  ovnsubaddlem1  47092  gpgvtxel2  48618  gpgvtx0  48623  gpgvtx1  48624  gpgedgvtx0  48631  gpgedgvtx1  48632  gpgvtxedg0  48633  gpgvtxedg1  48634  pgnbgreunbgrlem1  48683  pgnbgreunbgrlem2  48687  pgnbgreunbgrlem4  48689  pgnbgreunbgrlem5  48693  uspgrsprf  48716  uspgrsprf1  48717  dmmpossx2  48907  lmod1zr  49063  2arymaptf  49222  rrx2plordisom  49293  eloprab1st2nd  49437  funcf2lem  49650  oppf2  49709  tposcurf1  49868  reldmprcof2  49951  opf12  49973  setc1ocofval  50063