Theorem op2ndd 7927

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  Vcvv 3434  ⟨cop 4580  ‘cfv 6477  2^nd c2nd 7915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6433  df-fun 6479  df-fv 6485  df-2nd 7917

This theorem is referenced by:  2nd2val  7945  xp2nd  7949  sbcopeq1a  7976  csbopeq1a  7977  eloprabi  7990  mpomptsx  7991  dmmpossx  7993  fmpox  7994  ovmptss  8018  fmpoco  8020  df2nd2  8024  frxp  8051  xporderlem  8052  fnwelem  8056  fimaproj  8060  xpord2lem  8067  naddcllem  8586  xpf1o  9047  mapunen  9054  xpwdomg  9466  hsmexlem2  10310  nqereu  10812  uzrdgfni  13857  fsumcom2  15673  fprodcom2  15883  qredeu  16561  comfeq  17604  isfuncd  17764  cofucl  17787  funcres2b  17796  funcpropd  17801  xpcco2nd  18083  xpccatid  18086  1stf2  18091  2ndf2  18094  1stfcl  18095  2ndfcl  18096  prf2fval  18099  prfcl  18101  evlf2  18116  evlfcl  18120  curf12  18125  curf1cl  18126  curf2  18127  curfcl  18130  hof2fval  18153  hofcl  18157  txbas  23475  cnmpt2nd  23577  txhmeo  23711  ptuncnv  23715  ptunhmeo  23716  xpstopnlem1  23717  xkohmeo  23723  prdstmdd  24032  ucnimalem  24187  fmucndlem  24198  fsum2cn  24782  ovoliunlem1  25423  2sqreuop  27393  2sqreuopnn  27394  2sqreuoplt  27395  2sqreuopltb  27396  2sqreuopnnlt  27397  2sqreuopnnltb  27398  noseqrdgfn  28229  wlkl0  30337  fcnvgreu  32645  fsumiunle  32802  gsummpt2co  33018  gsumhashmul  33031  gsumwrd2dccatlem  33036  gsumwrd2dccat  33037  conjga  33129  elrgspnlem2  33200  elrgspnsubrunlem2  33205  mplvrpmga  33565  esumiun  34097  eulerpartlemgs2  34383  hgt750lemb  34659  satfv1  35375  satefvfmla0  35430  msubrsub  35538  msubco  35543  msubvrs  35572  filnetlem4  36394  finixpnum  37624  poimirlem4  37643  poimirlem15  37654  poimirlem20  37659  poimirlem26  37665  heicant  37674  heiborlem4  37833  heiborlem6  37835  dicelvalN  41196  aks6d1c2p1  42130  aks6d1c3  42135  aks6d1c4  42136  aks6d1c6lem2  42183  aks6d1c6lem4  42185  aks6d1c7lem1  42192  fmpocos  42246  rmxypairf1o  42923  unxpwdom3  43107  fgraphxp  43216  elcnvlem  43613  dvnprodlem2  45964  etransclem46  46297  ovnsubaddlem1  46587  gpgvtxel2  48058  gpgvtx0  48063  gpgvtx1  48064  gpgedgvtx0  48071  gpgedgvtx1  48072  gpgvtxedg0  48073  gpgvtxedg1  48074  pgnbgreunbgrlem1  48123  pgnbgreunbgrlem2  48127  pgnbgreunbgrlem4  48129  pgnbgreunbgrlem5  48133  uspgrsprf  48156  uspgrsprf1  48157  dmmpossx2  48347  lmod1zr  48504  2arymaptf  48663  rrx2plordisom  48734  eloprab1st2nd  48878  funcf2lem  49092  oppf2  49151  tposcurf1  49310  reldmprcof2  49393  opf12  49415  setc1ocofval  49505