NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  funfn GIF version

Theorem funfn 5136
Description: An equivalence for the function predicate. (Contributed by set.mm contributors, 13-Aug-2004.)
Assertion
Ref Expression
funfn (Fun AA Fn dom A)

Proof of Theorem funfn
StepHypRef Expression
1 eqid 2353 . . 3 dom A = dom A
21biantru 491 . 2 (Fun A ↔ (Fun A dom A = dom A))
3 df-fn 4790 . 2 (A Fn dom A ↔ (Fun A dom A = dom A))
42, 3bitr4i 243 1 (Fun AA Fn dom A)
Colors of variables: wff setvar class
Syntax hints:  wb 176   wa 358   = wceq 1642  dom cdm 4772  Fun wfun 4775   Fn wfn 4776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2346  df-fn 4790
This theorem is referenced by:  funssxp  5233  f1funfun  5263  funforn  5276  funbrfvb  5360  fvco  5383  eqfunfv  5397  fvimacnvi  5402  unpreima  5408  inpreima  5409  respreima  5410  ffvresb  5431  fnfullfun  5858  fvfullfun  5864  sbthlem1  6203  sbthlem3  6205
  Copyright terms: Public domain W3C validator