Theorem funfn 6579

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

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1539  dom cdm 5677  Fun wfun 6538   Fn wfn 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-fn 6547

This theorem is referenced by:  funfnd  6580  funssxp  6747  funforn  6813  funbrfvb  6947  funopfvb  6948  ssimaex  6977  fvco  6990  fvco4i  6993  eqfunfv  7038  fvimacnvi  7054  unpreima  7065  respreima  7068  elrnrexdm  7091  elrnrexdmb  7092  ffvresb  7127  funiun  7148  funressn  7160  funresdfunsn  7190  funex  7224  elunirn  7254  suppval1  8156  funsssuppss  8179  smores  8356  rdgsucg  8427  rdglimg  8429  imafi  9179  fundmfibi  9335  residfi  9337  mptfi  9355  ordtypelem6  9522  ordtypelem7  9523  harwdom  9590  ackbij2  10242  mptct  10537  smobeth  10585  hashkf  14298  hashfun  14403  fclim  15503  coapm  18027  psgnghm  21354  lindfrn  21597  elno3  27392  noextenddif  27405  noextendlt  27406  noextendgt  27407  nosupbnd2lem1  27452  noetasuplem4  27473  ausgrumgri  28692  dfnbgr3  28860  wlkiswwlks1  29386  vdn0conngrumgrv2  29714  hlimf  30755  adj1o  31412  abrexdomjm  32009  iunpreima  32061  fresf1o  32120  unipreima  32134  xppreima  32136  suppiniseg  32173  fdifsuppconst  32176  ressupprn  32177  mptctf  32207  orvcval2  33753  fineqvac  34393  fullfunfnv  35220  fullfunfv  35221  abrexdom  36903  diaf11N  40225  dibf11N  40337  gneispace3  43188  fresfo  46058  funbrafvb  46164  funopafvb  46165  funbrafv22b  46258  funopafv2b  46259