Theorem funfn 5247

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 2177	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 302	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5220	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 187	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1353  dom cdm 4627  Fun wfun 5211   Fn wfn 5212

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 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-fn 5220

This theorem is referenced by:  funfnd  5248  funssxp  5386  funforn  5446  funbrfvb  5559  funopfvb  5560  ssimaex  5578  fvco  5587  eqfunfv  5619  fvimacnvi  5631  unpreima  5642  respreima  5645  elrnrexdm  5656  elrnrexdmb  5657  ffvresb  5680  funresdfunsnss  5720  resfunexg  5738  funex  5740  elunirn  5767  smores  6293  smores2  6295  tfrlem1  6309  funresdfunsndc  6507  fundmfibi  6938  resunimafz0  10811  fclim  11302