Theorem funfn 6596

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 2737	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 529	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6564	. 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 5685  Fun wfun 6555   Fn wfn 6556

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  funfnd  6597  funssxp  6764  funforn  6827  funbrfvb  6962  funopfvb  6963  ssimaex  6994  fvco  7007  fvco4i  7010  eqfunfv  7056  fvimacnvi  7072  unpreima  7083  respreima  7086  elrnrexdm  7109  elrnrexdmb  7110  ffvresb  7145  funiun  7167  funressn  7179  funresdfunsn  7209  funex  7239  elunirn  7271  suppval1  8191  funsssuppss  8215  smores  8392  rdgsucg  8463  rdglimg  8465  imafiOLD  9354  fundmfibi  9376  residfi  9378  mptfi  9391  ordtypelem6  9563  ordtypelem7  9564  harwdom  9631  ackbij2  10282  mptct  10578  smobeth  10626  hashkf  14371  hashfun  14476  fclim  15589  coapm  18116  psgnghm  21598  lindfrn  21841  elno3  27700  noextenddif  27713  noextendlt  27714  noextendgt  27715  nosupbnd2lem1  27760  noetasuplem4  27781  ausgrumgri  29184  dfnbgr3  29355  wlkiswwlks1  29887  vdn0conngrumgrv2  30215  hlimf  31256  adj1o  31913  abrexdomjm  32526  iunpreima  32577  fresf1o  32641  unipreima  32653  xppreima  32655  suppiniseg  32695  fdifsuppconst  32698  ressupprn  32699  mptctf  32729  orvcval2  34461  fineqvac  35111  fullfunfnv  35947  fullfunfv  35948  abrexdom  37737  diaf11N  41051  dibf11N  41163  imadomfi  42003  gneispace3  44146  fresfo  47060  funbrafvb  47168  funopafvb  47169  funbrafv22b  47262  funopafv2b  47263  dfclnbgr3  47813  grimuhgr  47878