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

Theorem funeqi 5438
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 5437 . 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 1369   Fun wfun 5412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-in 3335  df-ss 3342  df-br 4293  df-opab 4351  df-rel 4847  df-cnv 4848  df-co 4849  df-fun 5420
This theorem is referenced by:  funmpt  5454  funmpt2  5455  funco  5456  fununfun  5462  funprg  5467  funtpg  5468  funtp  5470  f1cnvcnv  5614  f1co  5615  f10  5672  opabiotafun  5752  funoprabg  6189  mpt2fun  6192  ovidig  6208  funcnvuni  6530  fun11iun  6537  tposfun  6761  tfr1a  6853  tz7.44lem1  6861  tz7.48-2  6897  th3qcor  7208  ssdomg  7355  sbthlem7  7427  sbthlem8  7428  1sdom  7515  hartogslem1  7756  r1funlim  7973  zorn2lem4  8668  axaddf  9312  axmulf  9313  structfun  14186  strlemor1  14265  strleun  14268  fthoppc  14833  volf  21012  dfrelog  22017  0trl  23445  0pth  23469  1pthonlem1  23488  2pthlem1  23494  ajfuni  24260  hlimf  24640  funadj  25290  funcnvadj  25297  rinvf1o  25949  funcnvmptOLD  25986  frrlem10  27779  funpartfun  27974  funtransport  28062  funray  28171  funline  28173  funresfunco  30031  funcoressn  30033  bnj97  31859  bnj150  31869  bnj1384  32023  bnj1421  32033  bnj60  32053
  Copyright terms: Public domain W3C validator