Theorem funfn 6379

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 2821	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 532	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6352	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 280	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1533  dom cdm 5549  Fun wfun 6343   Fn wfn 6344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-fn 6352

This theorem is referenced by:  funfnd  6380  funssxp  6529  funforn  6591  funbrfvb  6714  funopfvb  6715  ssimaex  6742  fvco  6753  fvco4i  6756  eqfunfv  6801  fvimacnvi  6816  unpreima  6827  respreima  6830  elrnrexdm  6849  elrnrexdmb  6850  ffvresb  6882  funiun  6903  funressn  6915  funresdfunsn  6945  funex  6976  elunirn  7004  suppval1  7830  funsssuppss  7850  smores  7983  rdgsucg  8053  rdglimg  8055  fundmfibi  8797  residfi  8799  mptfi  8817  ordtypelem6  8981  ordtypelem7  8982  harwdom  9048  ackbij2  9659  mptct  9954  smobeth  10002  hashkf  13686  hashfun  13792  fclim  14904  coapm  17325  psgnghm  20718  lindfrn  20959  ausgrumgri  26946  dfnbgr3  27114  wlkiswwlks1  27639  vdn0conngrumgrv2  27969  hlimf  29008  adj1o  29665  abrexdomjm  30261  iunpreima  30310  fresf1o  30370  unipreima  30385  xppreima  30388  mptctf  30447  orvcval2  31711  elno3  33157  noextenddif  33170  noextendlt  33171  noextendgt  33172  nosupbnd2lem1  33210  noetalem3  33214  fullfunfnv  33402  fullfunfv  33403  abrexdom  34999  diaf11N  38179  dibf11N  38291  gneispace3  40476  funbrafvb  43349  funopafvb  43350  funbrafv22b  43443  funopafv2b  43444