Theorem funfn 3528

Description: An equivalence for the function predicate.

Assertion

Ref	Expression
funfn	|- (Fun A <-> A Fn dom A)

Proof of Theorem funfn

Step	Hyp	Ref	Expression
1		eqid 1468	. . 3 |- dom A = dom A
2	1	biantru 722	. 2 |- (Fun A <-> (Fun A /\ dom A = dom A))
3		df-fn 3183	. 2 |- (A Fn dom A <-> (Fun A /\ dom A = dom A))
4	2, 3	bitr4 176	1 |- (Fun A <-> A Fn dom A)

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 953  dom cdm 3160  Fun wfun 3166   Fn wfn 3167

This theorem is referenced by:  funex 3594  funssxp 3623  funforn 3663  ssimaex 3753  fvimacnvi 3789  elunirnALT 3854  brdom3 4773  brdom5 4774  brdom4 4775  adj1o 9735

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462  df-fn 3183

Copyright terms: Public domain