Theorem funfn 6608

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537  dom cdm 5700  Fun wfun 6567   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fn 6576

This theorem is referenced by:  funfnd  6609  funssxp  6776  funforn  6841  funbrfvb  6975  funopfvb  6976  ssimaex  7007  fvco  7020  fvco4i  7023  eqfunfv  7069  fvimacnvi  7085  unpreima  7096  respreima  7099  elrnrexdm  7123  elrnrexdmb  7124  ffvresb  7159  funiun  7181  funressn  7193  funresdfunsn  7223  funex  7256  elunirn  7288  suppval1  8207  funsssuppss  8231  smores  8408  rdgsucg  8479  rdglimg  8481  imafiOLD  9382  fundmfibi  9404  residfi  9406  mptfi  9421  ordtypelem6  9592  ordtypelem7  9593  harwdom  9660  ackbij2  10311  mptct  10607  smobeth  10655  hashkf  14381  hashfun  14486  fclim  15599  coapm  18138  psgnghm  21621  lindfrn  21864  elno3  27718  noextenddif  27731  noextendlt  27732  noextendgt  27733  nosupbnd2lem1  27778  noetasuplem4  27799  ausgrumgri  29202  dfnbgr3  29373  wlkiswwlks1  29900  vdn0conngrumgrv2  30228  hlimf  31269  adj1o  31926  abrexdomjm  32535  iunpreima  32587  fresf1o  32650  unipreima  32662  xppreima  32664  suppiniseg  32698  fdifsuppconst  32701  ressupprn  32702  mptctf  32731  orvcval2  34423  fineqvac  35073  fullfunfnv  35910  fullfunfv  35911  abrexdom  37690  diaf11N  41006  dibf11N  41118  imadomfi  41959  gneispace3  44095  fresfo  46963  funbrafvb  47071  funopafvb  47072  funbrafv22b  47165  funopafv2b  47166  dfclnbgr3  47699  grimuhgr  47762