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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ⟨cop 4573  ‘cfv 6498  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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fv 6506  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  48524  gpgvtx0  48529  gpgvtx1  48530  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  uspgrsprf  48622  uspgrsprf1  48623  dmmpossx2  48813  lmod1zr  48969  2arymaptf  49128  rrx2plordisom  49199  eloprab1st2nd  49343  funcf2lem  49556  oppf2  49615  tposcurf1  49774  reldmprcof2  49857  opf12  49879  setc1ocofval  49969