Theorem funfn 5407

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 5380	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 187	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   = wceq 1402  dom cdm 4774  Fun wfun 5371   Fn wfn 5372

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5380

This theorem is used by:  funfnd  5408  funssxp  5557  funforn  5622  funbrfvb  5743  funopfvb  5744  ssimaex  5764  fvco  5775  eqfunfv  5811  fvimacnvi  5823  unpreima  5833  respreima  5836  elrnrexdm  5847  elrnrexdmb  5848  ffvresb  5871  funiun  5890  funresdfunsnss  5918  resfunexg  5936  funex  5940  elunirn  5972  suppval1  6479  funsssuppss  6498  smores  6563  smores2  6565  tfrlem1  6579  funresdfunsndc  6779  fundmfibi  7252  resunimafz0  11274  fclim  12060  ausgrumgrien  16411