Theorem funfn 6568

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570  dom cdm 5663  Fun wfun 6532   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6541

This theorem is referenced by:  funfnd  6569  funssxp  6736  funforn  6801  funbrfvb  6936  funopfvb  6937  ssimaex  6968  fvco  6981  fvco4i  6985  eqfunfv  7033  fvimacnvi  7049  unpreima  7060  respreima  7063  elrnrexdm  7086  elrnrexdmb  7087  ffvresb  7123  funiun  7145  funressn  7158  funresdfunsn  7189  funex  7219  elunirn  7251  suppval1  8163  funsssuppss  8187  smores  8340  rdgsucg  8411  rdglimg  8413  fundmfibi  9294  residfi  9296  mptfi  9309  ordtypelem6  9486  ordtypelem7  9487  harwdom  9554  ackbij2  10226  mptct  10523  smobeth  10572  hashkf  14370  hashfun  14476  fclim  15606  coapm  18129  psgnghm  21711  lindfrn  21952  elno3  27800  noextenddif  27813  noextendlt  27814  noextendgt  27815  nosupbnd2lem1  27860  noetasuplem4  27881  ausgrumgri  29498  dfnbgr3  29669  wlkiswwlks1  30197  vdn0conngrumgrv2  30528  hlimf  31570  adj1o  32227  abrexdomjm  32834  iunpreima  32890  fresf1o  32957  unipreima  32969  xppreima  32971  rnressnsn  33003  suppiniseg  33012  fdifsuppconst  33015  ressupprn  33016  mptctf  33042  orvcval2  34830  fineqvac  35510  fullfunfnv  36419  fullfunfv  36420  abrexdom  38362  diaf11N  41804  dibf11N  41916  imadomfi  42750  gneispace3  44842  fresfo  47768  funbrafvb  47876  funopafvb  47877  funbrafv22b  47970  funopafv2b  47971  dfclnbgr3  48574  grimuhgr  48635