Theorem funfn 4451

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 1884	. . 3 |- dom A = dom A
2	1	biantru 793	. 2 |- (Fun A <-> (Fun A /\ dom A = dom A))
3		df-fn 4009	. 2 |- (A Fn dom A <-> (Fun A /\ dom A = dom A))
4	2, 3	bitr4i 193	1 |- (Fun A <-> A Fn dom A)

Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298  dom cdm 3986  Fun wfun 3992   Fn wfn 3993

This theorem is referenced by:  funex 4537  funssxp 4577  funforn 4624  ssimaex 4729  fvimacnvi 4777  elunirnALT 4845  brdom3 5963  brdom5 5964  brdom4 5965  adj1o 11455  eqfunfv 13839  wfrlem4 13960  axdenselem3 14021  inpreima 15682  unpreima 15683  respreima 15684  abrexdom 15739  smores 16446

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877  df-fn 4009

Copyright terms: Public domain