Theorem op2ndd 7954

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ⟨cop 4588  ‘cfv 6500  2^nd c2nd 7942

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fv 6508  df-2nd 7944

This theorem is referenced by:  2nd2val  7972  xp2nd  7976  sbcopeq1a  8003  csbopeq1a  8004  eloprabi  8017  mpomptsx  8018  dmmpossx  8020  fmpox  8021  ovmptss  8045  fmpoco  8047  df2nd2  8051  frxp  8078  xporderlem  8079  fnwelem  8083  fimaproj  8087  xpord2lem  8094  naddcllem  8614  xpf1o  9079  mapunen  9086  xpwdomg  9502  hsmexlem2  10349  nqereu  10852  uzrdgfni  13893  fsumcom2  15709  fprodcom2  15919  qredeu  16597  comfeq  17641  isfuncd  17801  cofucl  17824  funcres2b  17833  funcpropd  17838  xpcco2nd  18120  xpccatid  18123  1stf2  18128  2ndf2  18131  1stfcl  18132  2ndfcl  18133  prf2fval  18136  prfcl  18138  evlf2  18153  evlfcl  18157  curf12  18162  curf1cl  18163  curf2  18164  curfcl  18167  hof2fval  18190  hofcl  18194  txbas  23523  cnmpt2nd  23625  txhmeo  23759  ptuncnv  23763  ptunhmeo  23764  xpstopnlem1  23765  xkohmeo  23771  prdstmdd  24080  ucnimalem  24235  fmucndlem  24246  fsum2cn  24830  ovoliunlem1  25471  2sqreuop  27441  2sqreuopnn  27442  2sqreuoplt  27443  2sqreuopltb  27444  2sqreuopnnlt  27445  2sqreuopnnltb  27446  noseqrdgfn  28314  wlkl0  30454  fcnvgreu  32761  fsumiunle  32920  gsummpt2co  33141  gsumhashmul  33160  gsumwrd2dccatlem  33170  gsumwrd2dccat  33171  conjga  33263  elrgspnlem2  33336  elrgspnsubrunlem2  33341  mplvrpmga  33721  esumiun  34271  eulerpartlemgs2  34557  hgt750lemb  34833  satfv1  35576  satefvfmla0  35631  msubrsub  35739  msubco  35744  msubvrs  35773  filnetlem4  36594  finixpnum  37845  poimirlem4  37864  poimirlem15  37875  poimirlem20  37880  poimirlem26  37886  heicant  37895  heiborlem4  38054  heiborlem6  38056  dicelvalN  41543  aks6d1c2p1  42477  aks6d1c3  42482  aks6d1c4  42483  aks6d1c6lem2  42530  aks6d1c6lem4  42532  aks6d1c7lem1  42539  fmpocos  42595  rmxypairf1o  43257  unxpwdom3  43441  fgraphxp  43550  elcnvlem  43946  dvnprodlem2  46294  etransclem46  46627  ovnsubaddlem1  46917  gpgvtxel2  48397  gpgvtx0  48402  gpgvtx1  48403  gpgedgvtx0  48410  gpgedgvtx1  48411  gpgvtxedg0  48412  gpgvtxedg1  48413  pgnbgreunbgrlem1  48462  pgnbgreunbgrlem2  48466  pgnbgreunbgrlem4  48468  pgnbgreunbgrlem5  48472  uspgrsprf  48495  uspgrsprf1  48496  dmmpossx2  48686  lmod1zr  48842  2arymaptf  49001  rrx2plordisom  49072  eloprab1st2nd  49216  funcf2lem  49429  oppf2  49488  tposcurf1  49647  reldmprcof2  49730  opf12  49752  setc1ocofval  49842