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

Theorem funeqi 5824
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 5823 . 2 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
31, 2ax-mp 5 1 (Fun 𝐴 ↔ Fun 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  Fun wfun 5798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-fun 5806
This theorem is referenced by:  funmpt  5840  funmpt2  5841  funco  5842  fununfun  5848  funprg  5854  funprgOLD  5855  funtpg  5856  funtpgOLD  5857  funtp  5859  funcnvpr  5864  funcnvtp  5865  funcnvqp  5866  funcnvqpOLD  5867  funcnv0  5869  f1cnvcnv  6022  f1co  6023  f10  6081  opabiotafun  6169  fvn0ssdmfun  6258  funoprabg  6657  mpt2fun  6660  ovidig  6676  funcnvuni  7012  fun11iun  7019  tposfun  7255  tfr1a  7377  tz7.44lem1  7388  tz7.48-2  7424  ssdomg  7887  sbthlem7  7961  sbthlem8  7962  1sdom  8048  hartogslem1  8330  r1funlim  8512  zorn2lem4  9204  axaddf  9845  axmulf  9846  fundmge2nop0  13129  funcnvs1  13507  structfun  15707  strlemor1  15796  strleun  15799  fthoppc  16406  volf  23104  dfrelog  24116  0pth  26100  1pthonlem1  26119  2pthlem1  26125  ajfuni  27099  hlimf  27478  funadj  28129  funcnvadj  28136  rinvf1o  28814  funcnvmptOLD  28850  bnj97  30190  bnj150  30200  bnj1384  30354  bnj1421  30364  bnj60  30384  frrlem10  31035  funpartfun  31220  funtransport  31308  funray  31417  funline  31419  funresfunco  39854  funcoressn  39856  fpropnf1  40337  uhgr2edg  40435  usgredg3  40443  ushgredgedga  40456  ushgredgedgaloop  40458  2trld  41145  0pth-av  41293  1pthdlem1  41302  1trld  41309  3trld  41339
  Copyright terms: Public domain W3C validator