Theorem funfn 6598

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 2763	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 539	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6569	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 281	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  dom cdm 5658  Fun wfun 6560   Fn wfn 6561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-fn 6569

This theorem is used by:  funfnd  6599  funssxp  6768  funforn  6833  funbrfvb  6969  funopfvb  6970  ssimaex  7001  fvco  7014  fvco4i  7018  eqfunfv  7066  fvimacnvi  7082  unpreima  7094  respreima  7097  iunpreima  7100  elrnrexdm  7121  elrnrexdmb  7122  ffvresb  7158  funiun  7182  funressn  7195  funresdfunsn  7225  funex  7256  elunirn  7286  suppval1  8221  funsssuppss  8245  smores  8398  rdgsucg  8469  rdglimg  8471  fundmfibi  9363  residfi  9365  mptfi  9378  ordtypelem6  9554  ordtypelem7  9555  harwdom  9622  ackbij2  10359  imadomnum  10653  mptct  10661  smobeth  10710  hashkf  14517  hashfun  14623  fclim  15764  coapm  18296  psgnghm  21941  lindfrn  22182  elno3  28069  noextenddif  28082  noextendlt  28083  noextendgt  28084  nosupbnd2lem1  28129  noetasuplem4  28150  ausgrumgri  29805  dfnbgr3  29976  wlkiswwlks1  30513  vdn0conngrumgrv2  30854  hlimf  31896  adj1o  32553  abrexdomjm  33202  fresf1o  33323  unipreima  33335  xppreima  33337  rnressnsn  33368  suppiniseg  33376  fdifsuppconst  33379  ressupprn  33380  mptctf  33405  orvcval2  35202  fineqvac  35925  fullfunfnv  36925  fullfunfv  36926  abrexdom  38932  diaf11N  42372  dibf11N  42484  imadomfi  43318  gneispace3  45394  fresfo  48391  funbrafvb  48499  funopafvb  48500  funbrafv22b  48593  funopafv2b  48594  dfclnbgr3  49197  grimuhgr  49258