Theorem funfn 6567

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567  dom cdm 5662  Fun wfun 6531   Fn wfn 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-fn 6540

This theorem is referenced by:  funfnd  6568  funssxp  6735  funforn  6800  funbrfvb  6935  funopfvb  6936  ssimaex  6967  fvco  6980  fvco4i  6984  eqfunfv  7032  fvimacnvi  7048  unpreima  7059  respreima  7062  elrnrexdm  7085  elrnrexdmb  7086  ffvresb  7122  funiun  7144  funressn  7157  funresdfunsn  7188  funex  7218  elunirn  7250  suppval1  8162  funsssuppss  8186  smores  8339  rdgsucg  8410  rdglimg  8412  fundmfibi  9293  residfi  9295  mptfi  9308  ordtypelem6  9485  ordtypelem7  9486  harwdom  9553  ackbij2  10225  mptct  10522  smobeth  10571  hashkf  14368  hashfun  14474  fclim  15604  coapm  18128  psgnghm  21699  lindfrn  21940  elno3  27785  noextenddif  27798  noextendlt  27799  noextendgt  27800  nosupbnd2lem1  27845  noetasuplem4  27866  ausgrumgri  29458  dfnbgr3  29629  wlkiswwlks1  30157  vdn0conngrumgrv2  30488  hlimf  31530  adj1o  32187  abrexdomjm  32794  iunpreima  32850  fresf1o  32917  unipreima  32929  xppreima  32931  rnressnsn  32963  suppiniseg  32972  fdifsuppconst  32975  ressupprn  32976  mptctf  33002  orvcval2  34794  fineqvac  35452  fullfunfnv  36337  fullfunfv  36338  abrexdom  38269  diaf11N  41713  dibf11N  41825  imadomfi  42659  gneispace3  44751  fresfo  47674  funbrafvb  47782  funopafvb  47783  funbrafv22b  47876  funopafv2b  47877  dfclnbgr3  48480  grimuhgr  48541