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

Theorem funeqi 5599
Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
funeqi.1  |-  A  =  B
Assertion
Ref Expression
funeqi  |-  ( Fun 
A  <->  Fun  B )

Proof of Theorem funeqi
StepHypRef Expression
1 funeqi.1 . 2  |-  A  =  B
2 funeq 5598 . 2  |-  ( A  =  B  ->  ( Fun  A  <->  Fun  B ) )
31, 2ax-mp 5 1  |-  ( Fun 
A  <->  Fun  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1374   Fun wfun 5573
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-in 3476  df-ss 3483  df-br 4441  df-opab 4499  df-rel 4999  df-cnv 5000  df-co 5001  df-fun 5581
This theorem is referenced by:  funmpt  5615  funmpt2  5616  funco  5617  fununfun  5623  funprg  5628  funtpg  5629  funtp  5631  f1cnvcnv  5780  f1co  5781  f10  5838  opabiotafun  5919  funoprabg  6376  mpt2fun  6379  ovidig  6395  funcnvuni  6727  fun11iun  6734  tposfun  6961  tfr1a  7053  tz7.44lem1  7061  tz7.48-2  7097  ssdomg  7551  sbthlem7  7623  sbthlem8  7624  1sdom  7712  hartogslem1  7956  r1funlim  8173  zorn2lem4  8868  axaddf  9511  axmulf  9512  structfun  14491  strlemor1  14571  strleun  14574  fthoppc  15139  volf  21668  dfrelog  22674  0trl  24210  0pth  24234  1pthonlem1  24253  2pthlem1  24259  ajfuni  25437  hlimf  25817  funadj  26467  funcnvadj  26474  rinvf1o  27131  funcnvmptOLD  27167  frrlem10  28961  funpartfun  29156  funtransport  29244  funray  29353  funline  29355  funresfunco  31632  funcoressn  31634  bnj97  32878  bnj150  32888  bnj1384  33042  bnj1421  33052  bnj60  33072
  Copyright terms: Public domain W3C validator