Theorem funfn 6530

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  dom cdm 5632  Fun wfun 6494   Fn wfn 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6503

This theorem is referenced by:  funfnd  6531  funssxp  6698  funforn  6761  funbrfvb  6895  funopfvb  6896  ssimaex  6927  fvco  6940  fvco4i  6943  eqfunfv  6990  fvimacnvi  7006  unpreima  7017  respreima  7020  elrnrexdm  7043  elrnrexdmb  7044  ffvresb  7080  funiun  7102  funressn  7114  funresdfunsn  7145  funex  7175  elunirn  7207  suppval1  8118  funsssuppss  8142  smores  8294  rdgsucg  8364  rdglimg  8366  imafiOLD  9228  fundmfibi  9248  residfi  9250  mptfi  9263  ordtypelem6  9440  ordtypelem7  9441  harwdom  9508  ackbij2  10164  mptct  10460  smobeth  10509  hashkf  14267  hashfun  14372  fclim  15488  coapm  18007  psgnghm  21547  lindfrn  21788  elno3  27635  noextenddif  27648  noextendlt  27649  noextendgt  27650  nosupbnd2lem1  27695  noetasuplem4  27716  ausgrumgri  29252  dfnbgr3  29423  wlkiswwlks1  29952  vdn0conngrumgrv2  30283  hlimf  31324  adj1o  31981  abrexdomjm  32593  iunpreima  32650  fresf1o  32720  unipreima  32732  xppreima  32734  rnressnsn  32766  suppiniseg  32775  fdifsuppconst  32778  ressupprn  32779  mptctf  32805  orvcval2  34636  fineqvac  35291  fullfunfnv  36159  fullfunfv  36160  abrexdom  37978  diaf11N  41422  dibf11N  41534  imadomfi  42369  gneispace3  44486  fresfo  47405  funbrafvb  47513  funopafvb  47514  funbrafv22b  47607  funopafv2b  47608  dfclnbgr3  48183  grimuhgr  48244