Theorem op2ndd 7949

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3432  ⟨cop 4568  ‘cfv 6492  2^nd c2nd 7937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fv 6500  df-2nd 7939

This theorem is referenced by:  2nd2val  7967  xp2nd  7971  sbcopeq1a  7998  csbopeq1a  7999  eloprabi  8012  mpomptsx  8013  dmmpossx  8015  fmpox  8016  ovmptss  8039  fmpoco  8041  df2nd2  8045  frxp  8073  xporderlem  8074  fnwelem  8078  fimaproj  8082  xpord2lem  8089  naddcllem  8609  xpf1o  9074  mapunen  9081  xpwdomg  9497  hsmexlem2  10347  nqereu  10850  uzrdgfni  13918  fsumcom2  15734  fprodcom2  15947  qredeu  16625  comfeq  17670  isfuncd  17830  cofucl  17853  funcres2b  17862  funcpropd  17867  xpcco2nd  18149  xpccatid  18152  1stf2  18157  2ndf2  18160  1stfcl  18161  2ndfcl  18162  prf2fval  18165  prfcl  18167  evlf2  18182  evlfcl  18186  curf12  18191  curf1cl  18192  curf2  18193  curfcl  18196  hof2fval  18219  hofcl  18223  txbas  23557  cnmpt2nd  23659  txhmeo  23793  ptuncnv  23797  ptunhmeo  23798  xpstopnlem1  23799  xkohmeo  23805  prdstmdd  24114  ucnimalem  24269  fmucndlem  24280  fsum2cn  24863  ovoliunlem1  25494  2sqreuop  27450  2sqreuopnn  27451  2sqreuoplt  27452  2sqreuopltb  27453  2sqreuopnnlt  27454  2sqreuopnnltb  27455  noseqrdgfn  28323  wlkl0  30462  fcnvgreu  32771  fsumiunle  32928  gsummpt2co  33136  gsumhashmul  33155  gsumwrd2dccatlem  33165  gsumwrd2dccat  33166  conjga  33258  elrgspnlem2  33331  elrgspnsubrunlem2  33336  mplvrpmga  33736  esumiun  34285  eulerpartlemgs2  34571  hgt750lemb  34847  satfv1  35592  satefvfmla0  35647  msubrsub  35755  msubco  35760  msubvrs  35789  filnetlem4  36610  finixpnum  37973  poimirlem4  37992  poimirlem15  38003  poimirlem20  38008  poimirlem26  38014  heicant  38023  heiborlem4  38182  heiborlem6  38184  dicelvalN  41671  aks6d1c2p1  42604  aks6d1c3  42609  aks6d1c4  42610  aks6d1c6lem2  42657  aks6d1c6lem4  42659  aks6d1c7lem1  42666  fmpocos  42721  rmxypairf1o  43357  unxpwdom3  43541  fgraphxp  43650  elcnvlem  44046  dvnprodlem2  46391  etransclem46  46724  ovnsubaddlem1  47014  gpgvtxel2  48540  gpgvtx0  48545  gpgvtx1  48546  gpgedgvtx0  48553  gpgedgvtx1  48554  gpgvtxedg0  48555  gpgvtxedg1  48556  pgnbgreunbgrlem1  48605  pgnbgreunbgrlem2  48609  pgnbgreunbgrlem4  48611  pgnbgreunbgrlem5  48615  uspgrsprf  48638  uspgrsprf1  48639  dmmpossx2  48829  lmod1zr  48985  2arymaptf  49144  rrx2plordisom  49215  eloprab1st2nd  49359  funcf2lem  49572  oppf2  49631  tposcurf1  49790  reldmprcof2  49873  opf12  49895  setc1ocofval  49985