Theorem funfn 5243

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 5216	. 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 4624  Fun wfun 5207   Fn wfn 5208

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 5216

This theorem is referenced by:  funfnd  5244  funssxp  5382  funforn  5442  funbrfvb  5555  funopfvb  5556  ssimaex  5574  fvco  5583  eqfunfv  5615  fvimacnvi  5627  unpreima  5638  respreima  5641  elrnrexdm  5652  elrnrexdmb  5653  ffvresb  5676  funresdfunsnss  5716  resfunexg  5734  funex  5736  elunirn  5762  smores  6288  smores2  6290  tfrlem1  6304  funresdfunsndc  6502  fundmfibi  6933  resunimafz0  10802  fclim  11293