Theorem funfn 6546

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  dom cdm 5638  Fun wfun 6505   Fn wfn 6506

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6514

This theorem is referenced by:  funfnd  6547  funssxp  6716  funforn  6779  funbrfvb  6914  funopfvb  6915  ssimaex  6946  fvco  6959  fvco4i  6962  eqfunfv  7008  fvimacnvi  7024  unpreima  7035  respreima  7038  elrnrexdm  7061  elrnrexdmb  7062  ffvresb  7097  funiun  7119  funressn  7131  funresdfunsn  7163  funex  7193  elunirn  7225  suppval1  8145  funsssuppss  8169  smores  8321  rdgsucg  8391  rdglimg  8393  imafiOLD  9265  fundmfibi  9287  residfi  9289  mptfi  9302  ordtypelem6  9476  ordtypelem7  9477  harwdom  9544  ackbij2  10195  mptct  10491  smobeth  10539  hashkf  14297  hashfun  14402  fclim  15519  coapm  18033  psgnghm  21489  lindfrn  21730  elno3  27567  noextenddif  27580  noextendlt  27581  noextendgt  27582  nosupbnd2lem1  27627  noetasuplem4  27648  ausgrumgri  29094  dfnbgr3  29265  wlkiswwlks1  29797  vdn0conngrumgrv2  30125  hlimf  31166  adj1o  31823  abrexdomjm  32436  iunpreima  32493  fresf1o  32555  unipreima  32567  xppreima  32569  suppiniseg  32609  fdifsuppconst  32612  ressupprn  32613  mptctf  32641  orvcval2  34450  fineqvac  35087  fullfunfnv  35934  fullfunfv  35935  abrexdom  37724  diaf11N  41043  dibf11N  41155  imadomfi  41990  gneispace3  44122  fresfo  47049  funbrafvb  47157  funopafvb  47158  funbrafv22b  47251  funopafv2b  47252  dfclnbgr3  47827  grimuhgr  47887