Theorem funfn 6566

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 2735	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 529	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6534	. 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 5654  Fun wfun 6525   Fn wfn 6526

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  funfnd  6567  funssxp  6734  funforn  6797  funbrfvb  6932  funopfvb  6933  ssimaex  6964  fvco  6977  fvco4i  6980  eqfunfv  7026  fvimacnvi  7042  unpreima  7053  respreima  7056  elrnrexdm  7079  elrnrexdmb  7080  ffvresb  7115  funiun  7137  funressn  7149  funresdfunsn  7181  funex  7211  elunirn  7243  suppval1  8165  funsssuppss  8189  smores  8366  rdgsucg  8437  rdglimg  8439  imafiOLD  9326  fundmfibi  9348  residfi  9350  mptfi  9363  ordtypelem6  9537  ordtypelem7  9538  harwdom  9605  ackbij2  10256  mptct  10552  smobeth  10600  hashkf  14350  hashfun  14455  fclim  15569  coapm  18084  psgnghm  21540  lindfrn  21781  elno3  27619  noextenddif  27632  noextendlt  27633  noextendgt  27634  nosupbnd2lem1  27679  noetasuplem4  27700  ausgrumgri  29146  dfnbgr3  29317  wlkiswwlks1  29849  vdn0conngrumgrv2  30177  hlimf  31218  adj1o  31875  abrexdomjm  32488  iunpreima  32545  fresf1o  32609  unipreima  32621  xppreima  32623  suppiniseg  32663  fdifsuppconst  32666  ressupprn  32667  mptctf  32695  orvcval2  34491  fineqvac  35128  fullfunfnv  35964  fullfunfv  35965  abrexdom  37754  diaf11N  41068  dibf11N  41180  imadomfi  42015  gneispace3  44157  fresfo  47077  funbrafvb  47185  funopafvb  47186  funbrafv22b  47279  funopafv2b  47280  dfclnbgr3  47840  grimuhgr  47900