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

Theorem funeqi 6118
Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
funeqi.1 𝐴 = 𝐵
Assertion
Ref Expression
funeqi (Fun 𝐴 ↔ Fun 𝐵)

Proof of Theorem funeqi
StepHypRef Expression
1 funeqi.1 . 2 𝐴 = 𝐵
2 funeq 6117 . 2 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
31, 2ax-mp 5 1 (Fun 𝐴 ↔ Fun 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1637  Fun wfun 6091
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 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-in 3776  df-ss 3783  df-br 4845  df-opab 4907  df-rel 5318  df-cnv 5319  df-co 5320  df-fun 6099
This theorem is referenced by:  funmpt  6135  funmpt2  6136  funco  6137  funresfunco  6138  fununfun  6144  funprg  6150  funtpg  6151  funtp  6153  funcnvpr  6158  funcnvtp  6159  funcnvqp  6160  funcnv0  6162  f1cnvcnv  6321  f1co  6322  f10  6381  opabiotafun  6476  fvn0ssdmfun  6568  funopdmsn  6635  fpropnf1  6744  funoprabg  6985  mpt2fun  6988  ovidig  7004  funcnvuni  7345  fun11iun  7352  tposfun  7599  tfr1a  7722  tz7.44lem1  7733  tz7.48-2  7769  ssdomg  8234  sbthlem7  8311  sbthlem8  8312  1sdom  8398  hartogslem1  8682  r1funlim  8872  zorn2lem4  9602  axaddf  10247  axmulf  10248  fundmge2nop0  13487  funcnvs1  13877  strlemor1OLD  16176  strleun  16179  fthoppc  16783  cnfldfun  19962  cnfldfunALT  19963  cphsscph  23259  volf  23509  dfrelog  24525  usgredg3  26322  ushgredgedg  26335  ushgredgedgloop  26337  ushgredgedgloopOLD  26338  2trld  27077  0pth  27297  1pthdlem1  27307  1trld  27314  3trld  27344  ajfuni  28042  hlimf  28421  funadj  29072  funcnvadj  29079  rinvf1o  29758  funcnvmptOLD  29793  bnj97  31257  bnj150  31267  bnj1384  31421  bnj1421  31431  bnj60  31451  frrlem10  32110  funpartfun  32369  funtransport  32457  funray  32566  funline  32568  funcoressn  41658
  Copyright terms: Public domain W3C validator