Theorem funfn 5310

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1373  dom cdm 4683  Fun wfun 5274   Fn wfn 5275

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 1473  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-fn 5283

This theorem is referenced by:  funfnd  5311  funssxp  5455  funforn  5517  funbrfvb  5634  funopfvb  5635  ssimaex  5653  fvco  5662  eqfunfv  5695  fvimacnvi  5707  unpreima  5718  respreima  5721  elrnrexdm  5732  elrnrexdmb  5733  ffvresb  5756  funiun  5774  funresdfunsnss  5800  resfunexg  5818  funex  5820  elunirn  5848  smores  6391  smores2  6393  tfrlem1  6407  funresdfunsndc  6605  fundmfibi  7055  resunimafz0  10998  fclim  11680