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

Theorem funeqi 6349
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 6348 . 2 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
31, 2ax-mp 5 1 (Fun 𝐴 ↔ Fun 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  Fun wfun 6322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-br 5034  df-opab 5096  df-rel 5530  df-cnv 5531  df-co 5532  df-fun 6330
This theorem is referenced by:  funmpt  6366  funmpt2  6367  funco  6368  funresfunco  6369  fununfun  6376  funprg  6382  funtpg  6383  funtp  6385  funcnvpr  6390  funcnvtp  6391  funcnvqp  6392  funcnv0  6394  f1cnvcnv  6563  f1co  6564  opabiotafun  6723  fvn0ssdmfun  6823  funopdmsn  6893  fpropnf1  7007  funoprabg  7256  mpofun  7259  ovidig  7275  funcnvuni  7622  fiun  7630  f1iun  7631  tposfun  7895  tfr1a  8017  tz7.44lem1  8028  tz7.48-2  8065  ssdomg  8542  sbthlem7  8621  sbthlem8  8622  1sdom  8709  hartogslem1  8994  r1funlim  9183  zorn2lem4  9914  axaddf  10560  axmulf  10561  fundmge2nop0  13850  funcnvs1  14269  strleun  16586  fthoppc  17188  cnfldfun  20106  cnfldfunALT  20107  volf  24136  dfrelog  25160  usgredg3  27009  ushgredgedg  27022  ushgredgedgloop  27024  2trld  27727  0pth  27913  1pthdlem1  27923  1trld  27930  3trld  27960  ajfuni  28645  hlimf  29023  funadj  29672  funcnvadj  29679  rinvf1o  30392  bnj97  32246  bnj150  32256  bnj1384  32412  bnj1421  32422  bnj60  32442  satffunlem2lem2  32761  satfv0fvfmla0  32768  funpartfun  33512  funtransport  33600  funray  33709  funline  33711  bj-isrvec  34703  xlimfun  42484  funcoressn  43621
  Copyright terms: Public domain W3C validator