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