Theorem op2ndd 7995

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  Vcvv 3454  ⟨cop 4594  ‘cfv 6536  2^nd c2nd 7983

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-iota 6492  df-fun 6538  df-fv 6544  df-2nd 7985

This theorem is used by:  2nd2val  8013  xp2nd  8017  sbcopeq1a  8044  csbopeq1a  8045  eloprabi  8058  mpomptsx  8059  dmmpossx  8061  fmpox  8062  ovmptss  8086  fmpoco  8088  df2nd2  8092  frxp  8120  xporderlem  8121  fnwelem  8125  fimaproj  8129  xpord2lem  8136  naddcllem  8660  xpf1o  9125  mapunen  9132  xpwdomg  9545  hsmexlem2  10417  nqereu  10920  uzrdgfni  14001  fsumcom2  15832  fprodcom2  16045  qredeu  16722  comfeq  17768  isfuncd  17928  cofucl  17951  funcres2b  17960  funcpropd  17965  xpcco2nd  18247  xpccatid  18250  1stf2  18255  2ndf2  18258  1stfcl  18259  2ndfcl  18260  prf2fval  18263  prfcl  18265  evlf2  18280  evlfcl  18284  curf12  18289  curf1cl  18290  curf2  18291  curfcl  18294  hof2fval  18317  hofcl  18321  txbas  23735  cnmpt2nd  23837  txhmeo  23971  ptuncnv  23975  ptunhmeo  23976  xpstopnlem1  23977  xkohmeo  23983  prdstmdd  24292  ucnimalem  24447  fmucndlem  24458  fsum2cn  25041  ovoliunlem1  25672  2sqreuop  27637  2sqreuopnn  27638  2sqreuoplt  27639  2sqreuopltb  27640  2sqreuopnnlt  27641  2sqreuopnnltb  27642  noseqrdgfn  28510  wlkl0  30729  fcnvgreu  33028  fsumiunle  33184  gsummpt2co  33377  gsumhashmul  33396  gsumwrd2dccatlem  33406  gsumwrd2dccat  33407  conjga  33499  elrgspnlem2  33572  elrgspnsubrunlem2  33577  mplvrpmga  33944  esumiun  34493  eulerpartlemgs2  34779  hgt750lemb  35052  satfv1  35863  satefvfmla0  35918  msubrsub  36026  msubco  36031  msubvrs  36060  nmulprop  36690  filnetlem4  36920  finixpnum  38284  poimirlem4  38303  poimirlem15  38314  poimirlem20  38319  poimirlem26  38325  heicant  38334  heiborlem4  38493  heiborlem6  38495  dicelvalN  41980  aks6d1c2p1  42913  aks6d1c3  42918  aks6d1c4  42919  aks6d1c6lem2  42966  aks6d1c6lem4  42968  aks6d1c7lem1  42975  fmpocos  43032  rmxypairf1o  43666  unxpwdom3  43850  fgraphxp  43959  elcnvlem  44355  dvnprodlem2  46689  etransclem46  47022  ovnsubaddlem1  47312  gpgvtxel2  48841  gpgvtx0  48846  gpgvtx1  48847  gpgedgvtx0  48854  gpgedgvtx1  48855  gpgvtxedg0  48856  gpgvtxedg1  48857  pgnbgreunbgrlem1  48906  pgnbgreunbgrlem2  48910  pgnbgreunbgrlem4  48912  pgnbgreunbgrlem5  48916  uspgrsprf  48939  uspgrsprf1  48940  dmmpossx2  49145  lmod1zr  49301  2arymaptf  49460  rrx2plordisom  49531  eloprab1st2nd  49674  funcf2lem  49887  oppf2  49946  tposcurf1  50105  reldmprcof2  50188  opf12  50210  setc1ocofval  50300