Theorem funfn 5382

Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)

Assertion

Ref	Expression
funfn	⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Proof of Theorem funfn

Step	Hyp	Ref	Expression
1		eqid 2232	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 302	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5355	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 187	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1398  dom cdm 4749  Fun wfun 5346   Fn wfn 5347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1498  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-fn 5355

This theorem is referenced by:  funfnd  5383  funssxp  5532  funforn  5597  funbrfvb  5717  funopfvb  5718  ssimaex  5738  fvco  5747  eqfunfv  5780  fvimacnvi  5792  unpreima  5802  respreima  5805  elrnrexdm  5816  elrnrexdmb  5817  ffvresb  5840  funiun  5859  funresdfunsnss  5887  resfunexg  5905  funex  5909  elunirn  5939  suppval1  6439  funsssuppss  6458  smores  6523  smores2  6525  tfrlem1  6539  funresdfunsndc  6739  fundmfibi  7205  resunimafz0  11198  fclim  11979  ausgrumgrien  16165