Theorem funfn 6522

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  dom cdm 5624  Fun wfun 6486   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-fn 6495

This theorem is referenced by:  funfnd  6523  funssxp  6690  funforn  6753  funbrfvb  6887  funopfvb  6888  ssimaex  6919  fvco  6932  fvco4i  6935  eqfunfv  6981  fvimacnvi  6997  unpreima  7008  respreima  7011  elrnrexdm  7034  elrnrexdmb  7035  ffvresb  7070  funiun  7092  funressn  7104  funresdfunsn  7135  funex  7165  elunirn  7197  suppval1  8108  funsssuppss  8132  smores  8284  rdgsucg  8354  rdglimg  8356  imafiOLD  9216  fundmfibi  9236  residfi  9238  mptfi  9251  ordtypelem6  9428  ordtypelem7  9429  harwdom  9496  ackbij2  10152  mptct  10448  smobeth  10497  hashkf  14255  hashfun  14360  fclim  15476  coapm  17995  psgnghm  21535  lindfrn  21776  elno3  27623  noextenddif  27636  noextendlt  27637  noextendgt  27638  nosupbnd2lem1  27683  noetasuplem4  27704  ausgrumgri  29240  dfnbgr3  29411  wlkiswwlks1  29940  vdn0conngrumgrv2  30271  hlimf  31312  adj1o  31969  abrexdomjm  32582  iunpreima  32639  fresf1o  32709  unipreima  32721  xppreima  32723  rnressnsn  32756  suppiniseg  32765  fdifsuppconst  32768  ressupprn  32769  mptctf  32795  orvcval2  34616  fineqvac  35272  fullfunfnv  36140  fullfunfv  36141  abrexdom  37931  diaf11N  41309  dibf11N  41421  imadomfi  42256  gneispace3  44374  fresfo  47294  funbrafvb  47402  funopafvb  47403  funbrafv22b  47496  funopafv2b  47497  dfclnbgr3  48072  grimuhgr  48133