Theorem funfn 6576

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 2733	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 531	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6544	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 278	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542  dom cdm 5676  Fun wfun 6535   Fn wfn 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6544

This theorem is referenced by:  funfnd  6577  funssxp  6744  funforn  6810  funbrfvb  6944  funopfvb  6945  ssimaex  6974  fvco  6987  fvco4i  6990  eqfunfv  7035  fvimacnvi  7051  unpreima  7062  respreima  7065  elrnrexdm  7088  elrnrexdmb  7089  ffvresb  7121  funiun  7142  funressn  7154  funresdfunsn  7184  funex  7218  elunirn  7247  suppval1  8149  funsssuppss  8172  smores  8349  rdgsucg  8420  rdglimg  8422  imafi  9172  fundmfibi  9328  residfi  9330  mptfi  9348  ordtypelem6  9515  ordtypelem7  9516  harwdom  9583  ackbij2  10235  mptct  10530  smobeth  10578  hashkf  14289  hashfun  14394  fclim  15494  coapm  18018  psgnghm  21125  lindfrn  21368  elno3  27148  noextenddif  27161  noextendlt  27162  noextendgt  27163  nosupbnd2lem1  27208  noetasuplem4  27229  ausgrumgri  28417  dfnbgr3  28585  wlkiswwlks1  29111  vdn0conngrumgrv2  29439  hlimf  30478  adj1o  31135  abrexdomjm  31732  iunpreima  31784  fresf1o  31843  unipreima  31857  xppreima  31859  suppiniseg  31896  fdifsuppconst  31899  ressupprn  31900  mptctf  31930  orvcval2  33446  fineqvac  34086  fullfunfnv  34907  fullfunfv  34908  abrexdom  36587  diaf11N  39909  dibf11N  40021  gneispace3  42870  fresfo  45745  funbrafvb  45851  funopafvb  45852  funbrafv22b  45945  funopafv2b  45946