Theorem op2ndd 8012

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ⟨cop 4589  ‘cfv 6538  2^nd c2nd 8000

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-2nd 8002

This theorem is used by:  2nd2val  8030  xp2nd  8034  sbcopeq1a  8060  csbopeq1a  8061  eloprabi  8074  mpomptsx  8075  dmmpossx  8077  fmpox  8078  ovmptss  8104  fmpoco  8106  df2nd2  8110  frxp  8138  xporderlem  8139  fnwelem  8143  fimaproj  8152  xpord2lem  8159  naddcllem  8686  xpf1o  9159  mapunen  9166  xpwdomg  9580  hsmexlem2  10506  nqereu  11015  uzrdgfni  14102  fsumcom2  15941  fprodcom2  16152  qredeu  16834  comfeq  17881  isfuncd  18041  cofucl  18064  funcres2b  18073  funcpropd  18078  xpcco2nd  18360  xpccatid  18363  1stf2  18368  2ndf2  18371  1stfcl  18372  2ndfcl  18373  prf2fval  18376  prfcl  18378  evlf2  18393  evlfcl  18397  curf12  18402  curf1cl  18403  curf2  18404  curfcl  18407  hof2fval  18430  hofcl  18434  txbas  23887  cnmpt2nd  23989  txhmeo  24123  ptuncnv  24127  ptunhmeo  24128  xpstopnlem1  24129  xkohmeo  24135  prdstmdd  24444  ucnimalem  24599  fmucndlem  24610  fsum2cn  25193  ovoliunlem1  25824  2sqreuop  27790  2sqreuopnn  27791  2sqreuoplt  27792  2sqreuopltb  27793  2sqreuopnnlt  27794  2sqreuopnnltb  27795  noseqrdgfn  28693  wlkl0  30969  fcnvgreu  33309  fsumiunle  33463  gsummpt2co  33652  gsumhashmul  33671  gsumwrd2dccatlem  33681  gsumwrd2dccat  33682  conjga  33774  elrgspnlem2  33847  elrgspnsubrunlem2  33852  mplvrpmga  34220  esumiun  34769  eulerpartlemgs2  35055  hgt750lemb  35328  satfv1  36197  satefvfmla0  36252  msubrsub  36360  msubco  36365  msubvrs  36394  nmulprop  37014  filnetlem4  37244  finixpnum  38604  poimirlem4  38618  poimirlem15  38629  poimirlem20  38634  poimirlem26  38640  heicant  38649  heiborlem4  38824  heiborlem6  38826  dicelvalN  42311  aks6d1c2p1  43244  aks6d1c3  43249  aks6d1c4  43250  aks6d1c6lem2  43297  aks6d1c6lem4  43299  aks6d1c7lem1  43306  fmpocos  43363  rmxypairf1o  43994  unxpwdom3  44173  fgraphxp  44282  elcnvlem  44677  dvnprodlem2  47033  etransclem46  47366  ovnsubaddlem1  47656  gpgvtxel2  49222  gpgvtx0  49227  gpgvtx1  49228  gpgedgvtx0  49235  gpgedgvtx1  49236  gpgvtxedg0  49237  gpgvtxedg1  49238  pgnbgreunbgrlem1  49287  pgnbgreunbgrlem2  49291  pgnbgreunbgrlem4  49293  pgnbgreunbgrlem5  49297  uspgrsprf  49320  uspgrsprf1  49321  dmmpossx2  49525  lmod1zr  49681  2arymaptf  49840  rrx2plordisom  49911  eloprab1st2nd  50054  funcf2lem  50265  oppf2  50324  tposcurf1  50483  reldmprcof2  50566  opf12  50588  setc1ocofval  50678