Theorem op2ndd 8007

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  Vcvv 3463  ⟨cop 4612  ‘cfv 6541  2^nd c2nd 7995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-iota 6494  df-fun 6543  df-fv 6549  df-2nd 7997

This theorem is referenced by:  2nd2val  8025  xp2nd  8029  sbcopeq1a  8056  csbopeq1a  8057  eloprabi  8070  mpomptsx  8071  dmmpossx  8073  fmpox  8074  ovmptss  8100  fmpoco  8102  df2nd2  8106  frxp  8133  xporderlem  8134  fnwelem  8138  fimaproj  8142  xpord2lem  8149  naddcllem  8696  xpf1o  9161  mapunen  9168  xpwdomg  9607  hsmexlem2  10449  nqereu  10951  uzrdgfni  13981  fsumcom2  15793  fprodcom2  16003  qredeu  16678  comfeq  17721  isfuncd  17882  cofucl  17905  funcres2b  17914  funcpropd  17919  xpcco2nd  18201  xpccatid  18204  1stf2  18209  2ndf2  18212  1stfcl  18213  2ndfcl  18214  prf2fval  18217  prfcl  18219  evlf2  18234  evlfcl  18238  curf12  18243  curf1cl  18244  curf2  18245  curfcl  18248  hof2fval  18271  hofcl  18275  txbas  23522  cnmpt2nd  23624  txhmeo  23758  ptuncnv  23762  ptunhmeo  23763  xpstopnlem1  23764  xkohmeo  23770  prdstmdd  24079  ucnimalem  24235  fmucndlem  24246  fsum2cn  24832  ovoliunlem1  25474  2sqreuop  27443  2sqreuopnn  27444  2sqreuoplt  27445  2sqreuopltb  27446  2sqreuopnnlt  27447  2sqreuopnnltb  27448  noseqrdgfn  28249  wlkl0  30315  fcnvgreu  32619  fsumiunle  32776  gsummpt2co  32995  gsumhashmul  33008  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  elrgspnlem2  33191  elrgspnsubrunlem2  33196  esumiun  34070  eulerpartlemgs2  34357  hgt750lemb  34646  satfv1  35343  satefvfmla0  35398  msubrsub  35506  msubco  35511  msubvrs  35540  filnetlem4  36357  finixpnum  37587  poimirlem4  37606  poimirlem15  37617  poimirlem20  37622  poimirlem26  37628  heicant  37637  heiborlem4  37796  heiborlem6  37798  dicelvalN  41155  aks6d1c2p1  42094  aks6d1c3  42099  aks6d1c4  42100  aks6d1c6lem2  42147  aks6d1c6lem4  42149  aks6d1c7lem1  42156  fmpocos  42249  rmxypairf1o  42901  unxpwdom3  43085  fgraphxp  43194  elcnvlem  43591  dvnprodlem2  45934  etransclem46  46267  ovnsubaddlem1  46557  gpgvtxel2  47979  gpgvtx0  47981  gpgvtx1  47982  gpgedgvtx0  47992  gpgedgvtx1  47993  gpgvtxedg0  47994  gpgvtxedg1  47995  uspgrsprf  48035  uspgrsprf1  48036  dmmpossx2  48226  lmod1zr  48383  2arymaptf  48546  rrx2plordisom  48617  eloprab1st2nd  48751  funcf2lem  48939  tposcurf1  49044  setc1ocofval  49192