MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq2i Structured version   Visualization version   GIF version

Theorem feq2i 6374
Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011.)
Hypothesis
Ref Expression
feq2i.1 𝐴 = 𝐵
Assertion
Ref Expression
feq2i (𝐹:𝐴𝐶𝐹:𝐵𝐶)

Proof of Theorem feq2i
StepHypRef Expression
1 feq2i.1 . 2 𝐴 = 𝐵
2 feq2 6364 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2ax-mp 5 1 (𝐹:𝐴𝐶𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1522  wf 6221
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-fn 6228  df-f 6229
This theorem is referenced by:  fresaun  6417  fmpox  7621  fmpo  7622  tposf  7771  issmo  7837  axdc3lem4  9721  cardf  9818  smobeth  9854  seqf2  13239  hashfxnn0  13547  snopiswrd  13716  iswrddm0  13734  s1dm  13806  s2dm  14088  ntrivcvgtail  15089  vdwlem8  16153  0ram  16185  gsumws1  17815  ga0  18169  efgsp1  18590  efgsfo  18592  efgredleme  18596  efgred  18601  ablfaclem2  18925  islinds2  20639  pmatcollpw3fi1lem1  21078  0met  22659  dvef  24260  dvfsumrlim2  24312  dchrisum0  25778  trgcgrg  25983  tgcgr4  25999  axlowdimlem4  26414  uhgr0e  26539  vtxdumgrval  26951  wlkp1  27148  pthdlem2  27236  0wlk  27582  0spth  27592  0clwlkv  27597  wlk2v2e  27623  wlkl0  27838  padct  30143  mbfmcnt  31143  coinfliprv  31357  noxp1o  32779  matunitlindf  34421  fdc  34552  grposnOLD  34692  rabren3dioph  38897  amgm2d  40037  amgm3d  40038  fco3  41031  fourierdlem80  42013  sge0iun  42243  0ome  42353  issmflem  42546  2ffzoeq  43044  nnsum4primesodd  43443  nnsum4primesoddALTV  43444  nnsum4primeseven  43447  nnsum4primesevenALTV  43448  line2x  44222  line2y  44223  amgmw2d  44385
  Copyright terms: Public domain W3C validator