Theorem funfn 5402

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1402  dom cdm 4769  Fun wfun 5366   Fn wfn 5367

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 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5375

This theorem is referenced by:  funfnd  5403  funssxp  5552  funforn  5617  funbrfvb  5737  funopfvb  5738  ssimaex  5758  fvco  5769  eqfunfv  5802  fvimacnvi  5814  unpreima  5824  respreima  5827  elrnrexdm  5838  elrnrexdmb  5839  ffvresb  5862  funiun  5881  funresdfunsnss  5909  resfunexg  5927  funex  5931  elunirn  5962  suppval1  6469  funsssuppss  6488  smores  6553  smores2  6555  tfrlem1  6569  funresdfunsndc  6769  fundmfibi  7242  resunimafz0  11252  fclim  12038  ausgrumgrien  16325