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

Theorem funeqi 5474
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 5473 . 2  |-  ( A  =  B  ->  ( Fun  A  <->  Fun  B ) )
31, 2ax-mp 8 1  |-  ( Fun 
A  <->  Fun  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652   Fun wfun 5448
This theorem is referenced by:  funmpt  5489  funmpt2  5490  funco  5491  funprg  5500  funtpg  5501  funtp  5503  funcnvuni  5518  f1cnvcnv  5647  f1co  5648  fun11iun  5695  f10  5709  funoprabg  6169  mpt2fun  6172  ovidig  6191  tposfun  6495  opabiotafun  6536  tfr1a  6655  tz7.44lem1  6663  tz7.48-2  6699  abianfp  6716  th3qcor  7012  ssdomg  7153  sbthlem7  7223  sbthlem8  7224  1sdom  7311  hartogslem1  7511  r1funlim  7692  zorn2lem4  8379  axaddf  9020  axmulf  9021  structfun  13481  strlemor1  13556  strleun  13559  fthoppc  14120  volf  19425  dfrelog  20463  0trl  21546  0pth  21570  1pthonlem1  21589  2pthlem1  21595  ajfuni  22361  hlimf  22740  funadj  23389  funcnvadj  23396  rinvf1o  24042  funcnvmptOLD  24082  frrlem10  25593  funpartfun  25788  funtransport  25965  funray  26074  funline  26076  funresfunco  27965  funcoressn  27967  bnj97  29237  bnj150  29247  bnj1384  29401  bnj1421  29411  bnj60  29431
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-in 3327  df-ss 3334  df-br 4213  df-opab 4267  df-rel 4885  df-cnv 4886  df-co 4887  df-fun 5456
  Copyright terms: Public domain W3C validator