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

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542  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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  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  7124  funiun  7145  funressn  7157  funresdfunsn  7187  funex  7221  elunirn  7250  suppval1  8152  funsssuppss  8175  smores  8352  rdgsucg  8423  rdglimg  8425  imafi  9175  fundmfibi  9331  residfi  9333  mptfi  9351  ordtypelem6  9518  ordtypelem7  9519  harwdom  9586  ackbij2  10238  mptct  10533  smobeth  10581  hashkf  14292  hashfun  14397  fclim  15497  coapm  18021  psgnghm  21133  lindfrn  21376  elno3  27158  noextenddif  27171  noextendlt  27172  noextendgt  27173  nosupbnd2lem1  27218  noetasuplem4  27239  ausgrumgri  28427  dfnbgr3  28595  wlkiswwlks1  29121  vdn0conngrumgrv2  29449  hlimf  30490  adj1o  31147  abrexdomjm  31744  iunpreima  31796  fresf1o  31855  unipreima  31869  xppreima  31871  suppiniseg  31908  fdifsuppconst  31911  ressupprn  31912  mptctf  31942  orvcval2  33457  fineqvac  34097  fullfunfnv  34918  fullfunfv  34919  abrexdom  36598  diaf11N  39920  dibf11N  40032  gneispace3  42884  fresfo  45758  funbrafvb  45864  funopafvb  45865  funbrafv22b  45958  funopafv2b  45959