Theorem funfn 6516

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 2729	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 529	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6489	. 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 5623  Fun wfun 6480   Fn wfn 6481

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 2701

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

This theorem is referenced by:  funfnd  6517  funssxp  6684  funforn  6747  funbrfvb  6880  funopfvb  6881  ssimaex  6912  fvco  6925  fvco4i  6928  eqfunfv  6974  fvimacnvi  6990  unpreima  7001  respreima  7004  elrnrexdm  7027  elrnrexdmb  7028  ffvresb  7063  funiun  7085  funressn  7097  funresdfunsn  7129  funex  7159  elunirn  7191  suppval1  8106  funsssuppss  8130  smores  8282  rdgsucg  8352  rdglimg  8354  imafiOLD  9223  fundmfibi  9245  residfi  9247  mptfi  9260  ordtypelem6  9434  ordtypelem7  9435  harwdom  9502  ackbij2  10155  mptct  10451  smobeth  10499  hashkf  14257  hashfun  14362  fclim  15478  coapm  17996  psgnghm  21505  lindfrn  21746  elno3  27583  noextenddif  27596  noextendlt  27597  noextendgt  27598  nosupbnd2lem1  27643  noetasuplem4  27664  ausgrumgri  29130  dfnbgr3  29301  wlkiswwlks1  29830  vdn0conngrumgrv2  30158  hlimf  31199  adj1o  31856  abrexdomjm  32469  iunpreima  32526  fresf1o  32588  unipreima  32600  xppreima  32602  suppiniseg  32642  fdifsuppconst  32645  ressupprn  32646  mptctf  32674  orvcval2  34429  fineqvac  35074  fullfunfnv  35922  fullfunfv  35923  abrexdom  37712  diaf11N  41031  dibf11N  41143  imadomfi  41978  gneispace3  44109  fresfo  47036  funbrafvb  47144  funopafvb  47145  funbrafv22b  47238  funopafv2b  47239  dfclnbgr3  47814  grimuhgr  47875