Theorem funfn 6571

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 2760	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 539	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6542	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 281	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569  dom cdm 5650  Fun wfun 6533   Fn wfn 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fn 6542

This theorem is used by:  funfnd  6572  funssxp  6739  funforn  6804  funbrfvb  6939  funopfvb  6940  ssimaex  6971  fvco  6984  fvco4i  6988  eqfunfv  7036  fvimacnvi  7052  unpreima  7063  respreima  7066  iunpreima  7069  elrnrexdm  7090  elrnrexdmb  7091  ffvresb  7127  funiun  7151  funressn  7164  funresdfunsn  7195  funex  7226  elunirn  7256  suppval1  8187  funsssuppss  8211  smores  8364  rdgsucg  8435  rdglimg  8437  fundmfibi  9329  residfi  9331  mptfi  9344  ordtypelem6  9521  ordtypelem7  9522  harwdom  9589  ackbij2  10324  imadomnum  10618  mptct  10626  smobeth  10675  hashkf  14480  hashfun  14586  fclim  15726  coapm  18252  psgnghm  21892  lindfrn  22133  elno3  28018  noextenddif  28031  noextendlt  28032  noextendgt  28033  nosupbnd2lem1  28078  noetasuplem4  28099  ausgrumgri  29754  dfnbgr3  29925  wlkiswwlks1  30462  vdn0conngrumgrv2  30803  hlimf  31845  adj1o  32502  abrexdomjm  33151  fresf1o  33273  unipreima  33285  xppreima  33287  rnressnsn  33319  suppiniseg  33327  fdifsuppconst  33330  ressupprn  33331  mptctf  33356  orvcval2  35138  fineqvac  35841  fullfunfnv  36803  fullfunfv  36804  abrexdom  38758  diaf11N  42200  dibf11N  42312  imadomfi  43146  gneispace3  45227  fresfo  48212  funbrafvb  48320  funopafvb  48321  funbrafv22b  48414  funopafv2b  48415  dfclnbgr3  49018  grimuhgr  49079