Theorem op2ndd 7942

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3438  ⟨cop 4585  ‘cfv 6486  2^nd c2nd 7930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6442  df-fun 6488  df-fv 6494  df-2nd 7932

This theorem is referenced by:  2nd2val  7960  xp2nd  7964  sbcopeq1a  7991  csbopeq1a  7992  eloprabi  8005  mpomptsx  8006  dmmpossx  8008  fmpox  8009  ovmptss  8033  fmpoco  8035  df2nd2  8039  frxp  8066  xporderlem  8067  fnwelem  8071  fimaproj  8075  xpord2lem  8082  naddcllem  8601  xpf1o  9063  mapunen  9070  xpwdomg  9496  hsmexlem2  10340  nqereu  10842  uzrdgfni  13883  fsumcom2  15699  fprodcom2  15909  qredeu  16587  comfeq  17630  isfuncd  17790  cofucl  17813  funcres2b  17822  funcpropd  17827  xpcco2nd  18109  xpccatid  18112  1stf2  18117  2ndf2  18120  1stfcl  18121  2ndfcl  18122  prf2fval  18125  prfcl  18127  evlf2  18142  evlfcl  18146  curf12  18151  curf1cl  18152  curf2  18153  curfcl  18156  hof2fval  18179  hofcl  18183  txbas  23470  cnmpt2nd  23572  txhmeo  23706  ptuncnv  23710  ptunhmeo  23711  xpstopnlem1  23712  xkohmeo  23718  prdstmdd  24027  ucnimalem  24183  fmucndlem  24194  fsum2cn  24778  ovoliunlem1  25419  2sqreuop  27389  2sqreuopnn  27390  2sqreuoplt  27391  2sqreuopltb  27392  2sqreuopnnlt  27393  2sqreuopnnltb  27394  noseqrdgfn  28223  wlkl0  30329  fcnvgreu  32630  fsumiunle  32787  gsummpt2co  33014  gsumhashmul  33027  gsumwrd2dccatlem  33032  gsumwrd2dccat  33033  conjga  33125  elrgspnlem2  33193  elrgspnsubrunlem2  33198  esumiun  34060  eulerpartlemgs2  34347  hgt750lemb  34623  satfv1  35335  satefvfmla0  35390  msubrsub  35498  msubco  35503  msubvrs  35532  filnetlem4  36354  finixpnum  37584  poimirlem4  37603  poimirlem15  37614  poimirlem20  37619  poimirlem26  37625  heicant  37634  heiborlem4  37793  heiborlem6  37795  dicelvalN  41157  aks6d1c2p1  42091  aks6d1c3  42096  aks6d1c4  42097  aks6d1c6lem2  42144  aks6d1c6lem4  42146  aks6d1c7lem1  42153  fmpocos  42207  rmxypairf1o  42884  unxpwdom3  43068  fgraphxp  43177  elcnvlem  43574  dvnprodlem2  45929  etransclem46  46262  ovnsubaddlem1  46552  gpgvtxel2  48023  gpgvtx0  48028  gpgvtx1  48029  gpgedgvtx0  48036  gpgedgvtx1  48037  gpgvtxedg0  48038  gpgvtxedg1  48039  pgnbgreunbgrlem1  48087  pgnbgreunbgrlem2  48091  pgnbgreunbgrlem4  48093  pgnbgreunbgrlem5  48097  uspgrsprf  48118  uspgrsprf1  48119  dmmpossx2  48309  lmod1zr  48466  2arymaptf  48625  rrx2plordisom  48696  eloprab1st2nd  48840  funcf2lem  49054  oppf2  49113  tposcurf1  49272  reldmprcof2  49355  opf12  49377  setc1ocofval  49467