Theorem funfn 6448

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539  dom cdm 5580  Fun wfun 6412   Fn wfn 6413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fn 6421

This theorem is referenced by:  funfnd  6449  funssxp  6613  funforn  6679  funbrfvb  6806  funopfvb  6807  ssimaex  6835  fvco  6848  fvco4i  6851  eqfunfv  6896  fvimacnvi  6911  unpreima  6922  respreima  6925  elrnrexdm  6947  elrnrexdmb  6948  ffvresb  6980  funiun  7001  funressn  7013  funresdfunsn  7043  funex  7077  elunirn  7106  suppval1  7954  funsssuppss  7977  smores  8154  rdgsucg  8225  rdglimg  8227  imafi  8920  fundmfibi  9028  residfi  9030  mptfi  9048  ordtypelem6  9212  ordtypelem7  9213  harwdom  9280  ackbij2  9930  mptct  10225  smobeth  10273  hashkf  13974  hashfun  14080  fclim  15190  coapm  17702  psgnghm  20697  lindfrn  20938  ausgrumgri  27440  dfnbgr3  27608  wlkiswwlks1  28133  vdn0conngrumgrv2  28461  hlimf  29500  adj1o  30157  abrexdomjm  30753  iunpreima  30805  fresf1o  30867  unipreima  30882  xppreima  30884  suppiniseg  30922  fdifsuppconst  30925  ressupprn  30926  mptctf  30954  orvcval2  32325  fineqvac  32966  elno3  33785  noextenddif  33798  noextendlt  33799  noextendgt  33800  nosupbnd2lem1  33845  noetasuplem4  33866  fullfunfnv  34175  fullfunfv  34176  abrexdom  35815  diaf11N  38990  dibf11N  39102  gneispace3  41632  fresfo  44429  funbrafvb  44535  funopafvb  44536  funbrafv22b  44629  funopafv2b  44630