Theorem funfn 6597

Description: A class is a function if and only if it is a function on its domain. (Contributed by NM, 13-Aug-2004.)

Assertion

Ref	Expression
funfn	⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Proof of Theorem funfn

Step	Hyp	Ref	Expression
1		eqid 2734	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 529	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6565	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 278	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1536  dom cdm 5688  Fun wfun 6556   Fn wfn 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-fn 6565

This theorem is referenced by:  funfnd  6598  funssxp  6764  funforn  6827  funbrfvb  6961  funopfvb  6962  ssimaex  6993  fvco  7006  fvco4i  7009  eqfunfv  7055  fvimacnvi  7071  unpreima  7082  respreima  7085  elrnrexdm  7108  elrnrexdmb  7109  ffvresb  7144  funiun  7166  funressn  7178  funresdfunsn  7208  funex  7238  elunirn  7270  suppval1  8189  funsssuppss  8213  smores  8390  rdgsucg  8461  rdglimg  8463  imafiOLD  9351  fundmfibi  9373  residfi  9375  mptfi  9388  ordtypelem6  9560  ordtypelem7  9561  harwdom  9628  ackbij2  10279  mptct  10575  smobeth  10623  hashkf  14367  hashfun  14472  fclim  15585  coapm  18124  psgnghm  21615  lindfrn  21858  elno3  27714  noextenddif  27727  noextendlt  27728  noextendgt  27729  nosupbnd2lem1  27774  noetasuplem4  27795  ausgrumgri  29198  dfnbgr3  29369  wlkiswwlks1  29896  vdn0conngrumgrv2  30224  hlimf  31265  adj1o  31922  abrexdomjm  32534  iunpreima  32584  fresf1o  32647  unipreima  32659  xppreima  32661  suppiniseg  32700  fdifsuppconst  32703  ressupprn  32704  mptctf  32734  orvcval2  34439  fineqvac  35089  fullfunfnv  35927  fullfunfv  35928  abrexdom  37716  diaf11N  41031  dibf11N  41143  imadomfi  41983  gneispace3  44122  fresfo  46997  funbrafvb  47105  funopafvb  47106  funbrafv22b  47199  funopafv2b  47200  dfclnbgr3  47750  grimuhgr  47815