Theorem funfn 6528

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  dom cdm 5631  Fun wfun 6492   Fn wfn 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-fn 6501

This theorem is referenced by:  funfnd  6529  funssxp  6696  funforn  6759  funbrfvb  6893  funopfvb  6894  ssimaex  6925  fvco  6938  fvco4i  6941  eqfunfv  6988  fvimacnvi  7004  unpreima  7015  respreima  7018  elrnrexdm  7041  elrnrexdmb  7042  ffvresb  7078  funiun  7100  funressn  7113  funresdfunsn  7144  funex  7174  elunirn  7206  suppval1  8116  funsssuppss  8140  smores  8292  rdgsucg  8362  rdglimg  8364  imafiOLD  9226  fundmfibi  9246  residfi  9248  mptfi  9261  ordtypelem6  9438  ordtypelem7  9439  harwdom  9506  ackbij2  10164  mptct  10460  smobeth  10509  hashkf  14294  hashfun  14399  fclim  15515  coapm  18038  psgnghm  21560  lindfrn  21801  elno3  27619  noextenddif  27632  noextendlt  27633  noextendgt  27634  nosupbnd2lem1  27679  noetasuplem4  27700  ausgrumgri  29236  dfnbgr3  29407  wlkiswwlks1  29935  vdn0conngrumgrv2  30266  hlimf  31308  adj1o  31965  abrexdomjm  32577  iunpreima  32634  fresf1o  32704  unipreima  32716  xppreima  32718  rnressnsn  32750  suppiniseg  32759  fdifsuppconst  32762  ressupprn  32763  mptctf  32789  orvcval2  34603  fineqvac  35260  fullfunfnv  36128  fullfunfv  36129  abrexdom  38051  diaf11N  41495  dibf11N  41607  imadomfi  42441  gneispace3  44560  fresfo  47496  funbrafvb  47604  funopafvb  47605  funbrafv22b  47698  funopafv2b  47699  dfclnbgr3  48302  grimuhgr  48363