Theorem op2ndd 7953

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ⟨cop 4574  ‘cfv 6499  2^nd c2nd 7941

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5376  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6455  df-fun 6501  df-fv 6507  df-2nd 7943

This theorem is referenced by:  2nd2val  7971  xp2nd  7975  sbcopeq1a  8002  csbopeq1a  8003  eloprabi  8016  mpomptsx  8017  dmmpossx  8019  fmpox  8020  ovmptss  8043  fmpoco  8045  df2nd2  8049  frxp  8076  xporderlem  8077  fnwelem  8081  fimaproj  8085  xpord2lem  8092  naddcllem  8612  xpf1o  9077  mapunen  9084  xpwdomg  9500  hsmexlem2  10349  nqereu  10852  uzrdgfni  13920  fsumcom2  15736  fprodcom2  15949  qredeu  16627  comfeq  17672  isfuncd  17832  cofucl  17855  funcres2b  17864  funcpropd  17869  xpcco2nd  18151  xpccatid  18154  1stf2  18159  2ndf2  18162  1stfcl  18163  2ndfcl  18164  prf2fval  18167  prfcl  18169  evlf2  18184  evlfcl  18188  curf12  18193  curf1cl  18194  curf2  18195  curfcl  18198  hof2fval  18221  hofcl  18225  txbas  23532  cnmpt2nd  23634  txhmeo  23768  ptuncnv  23772  ptunhmeo  23773  xpstopnlem1  23774  xkohmeo  23780  prdstmdd  24089  ucnimalem  24244  fmucndlem  24255  fsum2cn  24838  ovoliunlem1  25469  2sqreuop  27425  2sqreuopnn  27426  2sqreuoplt  27427  2sqreuopltb  27428  2sqreuopnnlt  27429  2sqreuopnnltb  27430  noseqrdgfn  28298  wlkl0  30437  fcnvgreu  32745  fsumiunle  32902  gsummpt2co  33109  gsumhashmul  33128  gsumwrd2dccatlem  33138  gsumwrd2dccat  33139  conjga  33231  elrgspnlem2  33304  elrgspnsubrunlem2  33309  mplvrpmga  33689  esumiun  34238  eulerpartlemgs2  34524  hgt750lemb  34800  satfv1  35545  satefvfmla0  35600  msubrsub  35708  msubco  35713  msubvrs  35742  filnetlem4  36563  finixpnum  37926  poimirlem4  37945  poimirlem15  37956  poimirlem20  37961  poimirlem26  37967  heicant  37976  heiborlem4  38135  heiborlem6  38137  dicelvalN  41624  aks6d1c2p1  42557  aks6d1c3  42562  aks6d1c4  42563  aks6d1c6lem2  42610  aks6d1c6lem4  42612  aks6d1c7lem1  42619  fmpocos  42675  rmxypairf1o  43339  unxpwdom3  43523  fgraphxp  43632  elcnvlem  44028  dvnprodlem2  46375  etransclem46  46708  ovnsubaddlem1  46998  gpgvtxel2  48518  gpgvtx0  48523  gpgvtx1  48524  gpgedgvtx0  48531  gpgedgvtx1  48532  gpgvtxedg0  48533  gpgvtxedg1  48534  pgnbgreunbgrlem1  48583  pgnbgreunbgrlem2  48587  pgnbgreunbgrlem4  48589  pgnbgreunbgrlem5  48593  uspgrsprf  48616  uspgrsprf1  48617  dmmpossx2  48807  lmod1zr  48963  2arymaptf  49122  rrx2plordisom  49193  eloprab1st2nd  49337  funcf2lem  49550  oppf2  49609  tposcurf1  49768  reldmprcof2  49851  opf12  49873  setc1ocofval  49963