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

Theorem funeqi 5873
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 5872 . 2 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
31, 2ax-mp 5 1 (Fun 𝐴 ↔ Fun 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1480  Fun wfun 5846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-in 3566  df-ss 3573  df-br 4619  df-opab 4679  df-rel 5086  df-cnv 5087  df-co 5088  df-fun 5854
This theorem is referenced by:  funmpt  5889  funmpt2  5890  funco  5891  fununfun  5897  funprg  5903  funprgOLD  5904  funtpg  5905  funtpgOLD  5906  funtp  5908  funcnvpr  5913  funcnvtp  5914  funcnvqp  5915  funcnvqpOLD  5916  funcnv0  5918  f1cnvcnv  6071  f1co  6072  f10  6131  opabiotafun  6221  fvn0ssdmfun  6311  funopdmsn  6375  fpropnf1  6484  funoprabg  6719  mpt2fun  6722  ovidig  6738  funcnvuni  7073  fun11iun  7080  tposfun  7320  tfr1a  7442  tz7.44lem1  7453  tz7.48-2  7489  ssdomg  7953  sbthlem7  8028  sbthlem8  8029  1sdom  8115  hartogslem1  8399  r1funlim  8581  zorn2lem4  9273  axaddf  9918  axmulf  9919  fundmge2nop0  13221  funcnvs1  13601  strlemor1OLD  15901  strleun  15904  fthoppc  16515  cnfldfun  19690  cnfldfunALT  19691  volf  23220  dfrelog  24233  uhgr2edg  26010  usgredg3  26018  ushgredgedg  26031  ushgredgedgloop  26033  2trld  26720  0pth  26869  1pthdlem1  26878  1trld  26885  3trld  26915  ajfuni  27585  hlimf  27964  funadj  28615  funcnvadj  28622  rinvf1o  29299  funcnvmptOLD  29333  bnj97  30679  bnj150  30689  bnj1384  30843  bnj1421  30853  bnj60  30873  frrlem10  31527  funpartfun  31727  funtransport  31815  funray  31924  funline  31926  funresfunco  40535  funcoressn  40537
  Copyright terms: Public domain W3C validator