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

Theorem funeqi 5594
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 5593 . 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 1381   Fun wfun 5568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-in 3465  df-ss 3472  df-br 4434  df-opab 4492  df-rel 4992  df-cnv 4993  df-co 4994  df-fun 5576
This theorem is referenced by:  funmpt  5610  funmpt2  5611  funco  5612  fununfun  5618  funprg  5623  funtpg  5624  funtp  5626  f1cnvcnv  5775  f1co  5776  f10  5833  opabiotafun  5915  fvn0ssdmfun  6003  funoprabg  6382  mpt2fun  6385  ovidig  6401  funcnvuni  6734  fun11iun  6741  tposfun  6969  tfr1a  7061  tz7.44lem1  7069  tz7.48-2  7105  ssdomg  7559  sbthlem7  7631  sbthlem8  7632  1sdom  7720  hartogslem1  7965  r1funlim  8182  zorn2lem4  8877  axaddf  9520  axmulf  9521  structfun  14516  strlemor1  14596  strleun  14599  fthoppc  15161  volf  21806  dfrelog  22818  0trl  24413  0pth  24437  1pthonlem1  24456  2pthlem1  24462  ajfuni  25640  hlimf  26020  funadj  26670  funcnvadj  26677  rinvf1o  27337  funcnvmptOLD  27374  frrlem10  29366  funpartfun  29561  funtransport  29649  funray  29758  funline  29760  funresfunco  32044  funcoressn  32046  bnj97  33631  bnj150  33641  bnj1384  33795  bnj1421  33805  bnj60  33825
  Copyright terms: Public domain W3C validator