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

Theorem funeqi 6053
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 6052 . 2 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
31, 2ax-mp 5 1 (Fun 𝐴 ↔ Fun 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1631  Fun wfun 6026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-in 3731  df-ss 3738  df-br 4788  df-opab 4848  df-rel 5257  df-cnv 5258  df-co 5259  df-fun 6034
This theorem is referenced by:  funmpt  6070  funmpt2  6071  funco  6072  fununfun  6078  funprg  6084  funtpg  6085  funtp  6087  funcnvpr  6092  funcnvtp  6093  funcnvqp  6094  funcnv0  6096  f1cnvcnv  6251  f1co  6252  f10  6311  opabiotafun  6402  fvn0ssdmfun  6494  funopdmsn  6559  fpropnf1  6668  funoprabg  6907  mpt2fun  6910  ovidig  6926  funcnvuni  7267  fun11iun  7274  tposfun  7521  tfr1a  7644  tz7.44lem1  7655  tz7.48-2  7691  ssdomg  8156  sbthlem7  8233  sbthlem8  8234  1sdom  8320  hartogslem1  8604  r1funlim  8794  zorn2lem4  9524  axaddf  10169  axmulf  10170  fundmge2nop0  13477  funcnvs1  13867  strlemor1OLD  16178  strleun  16181  fthoppc  16791  cnfldfun  19974  cnfldfunALT  19975  volf  23518  dfrelog  24534  usgredg3  26331  ushgredgedg  26344  ushgredgedgloop  26346  ushgredgedgloopOLD  26347  2trld  27086  0pth  27306  1pthdlem1  27316  1trld  27323  3trld  27353  ajfuni  28056  hlimf  28435  funadj  29086  funcnvadj  29093  rinvf1o  29773  funcnvmptOLD  29808  bnj97  31275  bnj150  31285  bnj1384  31439  bnj1421  31449  bnj60  31469  frrlem10  32129  funpartfun  32388  funtransport  32476  funray  32585  funline  32587  funresfunco  41726  funcoressn  41728
  Copyright terms: Public domain W3C validator