Theorem funfn 6507

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  dom cdm 5614  Fun wfun 6471   Fn wfn 6472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722  df-fn 6480

This theorem is referenced by:  funfnd  6508  funssxp  6675  funforn  6738  funbrfvb  6870  funopfvb  6871  ssimaex  6902  fvco  6915  fvco4i  6918  eqfunfv  6964  fvimacnvi  6980  unpreima  6991  respreima  6994  elrnrexdm  7017  elrnrexdmb  7018  ffvresb  7053  funiun  7075  funressn  7087  funresdfunsn  7118  funex  7148  elunirn  7180  suppval1  8091  funsssuppss  8115  smores  8267  rdgsucg  8337  rdglimg  8339  imafiOLD  9195  fundmfibi  9215  residfi  9217  mptfi  9230  ordtypelem6  9404  ordtypelem7  9405  harwdom  9472  ackbij2  10125  mptct  10421  smobeth  10469  hashkf  14231  hashfun  14336  fclim  15452  coapm  17970  psgnghm  21510  lindfrn  21751  elno3  27587  noextenddif  27600  noextendlt  27601  noextendgt  27602  nosupbnd2lem1  27647  noetasuplem4  27668  ausgrumgri  29138  dfnbgr3  29309  wlkiswwlks1  29838  vdn0conngrumgrv2  30166  hlimf  31207  adj1o  31864  abrexdomjm  32477  iunpreima  32534  fresf1o  32603  unipreima  32615  xppreima  32617  suppiniseg  32657  fdifsuppconst  32660  ressupprn  32661  mptctf  32689  orvcval2  34462  fineqvac  35107  fullfunfnv  35959  fullfunfv  35960  abrexdom  37749  diaf11N  41067  dibf11N  41179  imadomfi  42014  gneispace3  44145  fresfo  47058  funbrafvb  47166  funopafvb  47167  funbrafv22b  47260  funopafv2b  47261  dfclnbgr3  47836  grimuhgr  47897