Theorem funfn 6549

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  dom cdm 5641  Fun wfun 6508   Fn wfn 6509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  funfnd  6550  funssxp  6719  funforn  6782  funbrfvb  6917  funopfvb  6918  ssimaex  6949  fvco  6962  fvco4i  6965  eqfunfv  7011  fvimacnvi  7027  unpreima  7038  respreima  7041  elrnrexdm  7064  elrnrexdmb  7065  ffvresb  7100  funiun  7122  funressn  7134  funresdfunsn  7166  funex  7196  elunirn  7228  suppval1  8148  funsssuppss  8172  smores  8324  rdgsucg  8394  rdglimg  8396  imafiOLD  9272  fundmfibi  9294  residfi  9296  mptfi  9309  ordtypelem6  9483  ordtypelem7  9484  harwdom  9551  ackbij2  10202  mptct  10498  smobeth  10546  hashkf  14304  hashfun  14409  fclim  15526  coapm  18040  psgnghm  21496  lindfrn  21737  elno3  27574  noextenddif  27587  noextendlt  27588  noextendgt  27589  nosupbnd2lem1  27634  noetasuplem4  27655  ausgrumgri  29101  dfnbgr3  29272  wlkiswwlks1  29804  vdn0conngrumgrv2  30132  hlimf  31173  adj1o  31830  abrexdomjm  32443  iunpreima  32500  fresf1o  32562  unipreima  32574  xppreima  32576  suppiniseg  32616  fdifsuppconst  32619  ressupprn  32620  mptctf  32648  orvcval2  34457  fineqvac  35094  fullfunfnv  35941  fullfunfv  35942  abrexdom  37731  diaf11N  41050  dibf11N  41162  imadomfi  41997  gneispace3  44129  fresfo  47053  funbrafvb  47161  funopafvb  47162  funbrafv22b  47255  funopafv2b  47256  dfclnbgr3  47831  grimuhgr  47891