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

Theorem feq1i 6245
Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq1i.1 𝐹 = 𝐺
Assertion
Ref Expression
feq1i (𝐹:𝐴𝐵𝐺:𝐴𝐵)

Proof of Theorem feq1i
StepHypRef Expression
1 feq1i.1 . 2 𝐹 = 𝐺
2 feq1 6235 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2ax-mp 5 1 (𝐹:𝐴𝐵𝐺:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1637  wf 6095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-rab 3103  df-v 3391  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4843  df-opab 4905  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-fun 6101  df-fn 6102  df-f 6103
This theorem is referenced by:  ftpg  6645  fpropnf1  6746  suppsnop  7541  seqomlem2  7780  addnqf  10053  mulnqf  10054  hashfOLD  13344  isumsup2  14798  ruclem6  15182  sadcf  15392  sadadd2lem  15398  sadadd3  15400  sadaddlem  15405  smupf  15417  algrf  15503  funcoppc  16737  pmtr3ncomlem1  18092  znf1o  20105  ovolfsf  23450  ovolsf  23451  ovoliunlem1  23481  ovoliun  23484  ovoliun2  23485  voliunlem3  23531  itgss3  23793  dvexp  23928  efcn  24409  gamf  24981  basellem9  25027  axlowdimlem10  26043  wlkres  26793  1wlkdlem1  27308  vsfval  27814  ho0f  28936  opsqrlem4  29328  pjinvari  29376  fmptdF  29781  omssubaddlem  30684  omssubadd  30685  sitgclg  30727  sitgaddlemb  30733  coinfliprv  30867  plymul02  30946  signshf  30988  circum  31888  knoppcnlem8  32805  knoppcnlem11  32808  poimirlem31  33751  diophren  37877  clsf2  38922  seff  39006  binomcxplemnotnn0  39053  volicoff  40689  fourierdlem62  40862  fourierdlem80  40880  fourierdlem97  40897  carageniuncllem2  41216  0ome  41223  mapprop  42690  lindslinindimp2lem2  42814  zlmodzxzldeplem1  42855
  Copyright terms: Public domain W3C validator