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

Theorem funeqi 5533
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 5532 . 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 1399   Fun wfun 5507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-in 3413  df-ss 3420  df-br 4385  df-opab 4443  df-rel 4937  df-cnv 4938  df-co 4939  df-fun 5515
This theorem is referenced by:  funmpt  5549  funmpt2  5550  funco  5551  fununfun  5557  funprg  5562  funtpg  5563  funtp  5565  f1cnvcnv  5714  f1co  5715  f10  5772  opabiotafun  5852  fvn0ssdmfun  5941  funoprabg  6322  mpt2fun  6325  ovidig  6341  funcnvuni  6674  fun11iun  6681  tposfun  6911  tfr1a  7003  tz7.44lem1  7011  tz7.48-2  7047  ssdomg  7502  sbthlem7  7574  sbthlem8  7575  1sdom  7661  hartogslem1  7904  r1funlim  8119  zorn2lem4  8814  axaddf  9455  axmulf  9456  structfun  14669  strlemor1  14752  strleun  14755  fthoppc  15352  volf  22048  dfrelog  23061  0trl  24694  0pth  24718  1pthonlem1  24737  2pthlem1  24743  ajfuni  25917  hlimf  26297  funadj  26946  funcnvadj  26953  rinvf1o  27644  funcnvmptOLD  27689  frrlem10  29603  funpartfun  29786  funtransport  29874  funray  29983  funline  29985  funresfunco  32415  funcoressn  32417  bnj97  34310  bnj150  34320  bnj1384  34474  bnj1421  34484  bnj60  34504
  Copyright terms: Public domain W3C validator