Theorem op2ndd 7682

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3441  ⟨cop 4531  ‘cfv 6324  2^nd c2nd 7670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6283  df-fun 6326  df-fv 6332  df-2nd 7672

This theorem is referenced by:  2nd2val  7700  xp2nd  7704  sbcopeq1a  7730  csbopeq1a  7731  eloprabi  7743  mpomptsx  7744  dmmpossx  7746  fmpox  7747  ovmptss  7771  fmpoco  7773  df2nd2  7777  frxp  7803  xporderlem  7804  fnwelem  7808  fimaproj  7812  xpf1o  8663  mapunen  8670  xpwdomg  9033  hsmexlem2  9838  nqereu  10340  uzrdgfni  13321  fsumcom2  15121  fprodcom2  15330  qredeu  15992  comfeq  16968  isfuncd  17127  cofucl  17150  funcres2b  17159  funcpropd  17162  xpcco2nd  17427  xpccatid  17430  1stf2  17435  2ndf2  17438  1stfcl  17439  2ndfcl  17440  prf2fval  17443  prfcl  17445  evlf2  17460  evlfcl  17464  curf12  17469  curf1cl  17470  curf2  17471  curfcl  17474  hof2fval  17497  hofcl  17501  txbas  22172  cnmpt2nd  22274  txhmeo  22408  ptuncnv  22412  ptunhmeo  22413  xpstopnlem1  22414  xkohmeo  22420  prdstmdd  22729  ucnimalem  22886  fmucndlem  22897  fsum2cn  23476  ovoliunlem1  24106  2sqreuop  26046  2sqreuopnn  26047  2sqreuoplt  26048  2sqreuopltb  26049  2sqreuopnnlt  26050  2sqreuopnnltb  26051  wlkl0  28152  fcnvgreu  30436  fsumiunle  30571  gsummpt2co  30733  gsumhashmul  30741  esumiun  31463  eulerpartlemgs2  31748  hgt750lemb  32037  satfv1  32723  satefvfmla0  32778  msubrsub  32886  msubco  32891  msubvrs  32920  filnetlem4  33842  finixpnum  35042  poimirlem4  35061  poimirlem15  35072  poimirlem20  35077  poimirlem26  35083  heicant  35092  heiborlem4  35252  heiborlem6  35254  dicelvalN  38474  rmxypairf1o  39852  unxpwdom3  40039  fgraphxp  40155  elcnvlem  40301  dvnprodlem2  42589  etransclem46  42922  ovnsubaddlem1  43209  uspgrsprf  44374  uspgrsprf1  44375  dmmpossx2  44738  lmod1zr  44902  2arymaptf  45066  rrx2plordisom  45137