Theorem funfn 6511

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 2731	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 529	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6484	. 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 5616  Fun wfun 6475   Fn wfn 6476

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 2121  ax-ext 2703

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

This theorem is referenced by:  funfnd  6512  funssxp  6679  funforn  6742  funbrfvb  6875  funopfvb  6876  ssimaex  6907  fvco  6920  fvco4i  6923  eqfunfv  6969  fvimacnvi  6985  unpreima  6996  respreima  6999  elrnrexdm  7022  elrnrexdmb  7023  ffvresb  7058  funiun  7080  funressn  7092  funresdfunsn  7123  funex  7153  elunirn  7185  suppval1  8096  funsssuppss  8120  smores  8272  rdgsucg  8342  rdglimg  8344  imafiOLD  9200  fundmfibi  9220  residfi  9222  mptfi  9235  ordtypelem6  9409  ordtypelem7  9410  harwdom  9477  ackbij2  10133  mptct  10429  smobeth  10477  hashkf  14239  hashfun  14344  fclim  15460  coapm  17978  psgnghm  21518  lindfrn  21759  elno3  27595  noextenddif  27608  noextendlt  27609  noextendgt  27610  nosupbnd2lem1  27655  noetasuplem4  27676  ausgrumgri  29146  dfnbgr3  29317  wlkiswwlks1  29846  vdn0conngrumgrv2  30174  hlimf  31215  adj1o  31872  abrexdomjm  32485  iunpreima  32542  fresf1o  32611  unipreima  32623  xppreima  32625  suppiniseg  32665  fdifsuppconst  32668  ressupprn  32669  mptctf  32697  orvcval2  34470  fineqvac  35137  fullfunfnv  35986  fullfunfv  35987  abrexdom  37776  diaf11N  41094  dibf11N  41206  imadomfi  42041  gneispace3  44172  fresfo  47085  funbrafvb  47193  funopafvb  47194  funbrafv22b  47287  funopafv2b  47288  dfclnbgr3  47863  grimuhgr  47924