Theorem funfn 6563

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 6536	. 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 1570  dom cdm 5655  Fun wfun 6527   Fn wfn 6528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  funfnd  6564  funssxp  6731  funforn  6796  funbrfvb  6931  funopfvb  6932  ssimaex  6963  fvco  6976  fvco4i  6980  eqfunfv  7028  fvimacnvi  7044  unpreima  7055  respreima  7058  iunpreima  7061  elrnrexdm  7082  elrnrexdmb  7083  ffvresb  7119  funiun  7143  funressn  7156  funresdfunsn  7187  funex  7218  elunirn  7248  suppval1  8164  funsssuppss  8188  smores  8341  rdgsucg  8412  rdglimg  8414  fundmfibi  9303  residfi  9305  mptfi  9318  ordtypelem6  9495  ordtypelem7  9496  harwdom  9563  ackbij2  10244  imadomnum  10538  mptct  10546  smobeth  10595  hashkf  14396  hashfun  14502  fclim  15640  coapm  18160  psgnghm  21793  lindfrn  22034  elno3  27891  noextenddif  27904  noextendlt  27905  noextendgt  27906  nosupbnd2lem1  27951  noetasuplem4  27972  ausgrumgri  29627  dfnbgr3  29798  wlkiswwlks1  30335  vdn0conngrumgrv2  30676  hlimf  31718  adj1o  32375  abrexdomjm  32982  fresf1o  33104  unipreima  33116  xppreima  33118  rnressnsn  33150  suppiniseg  33158  fdifsuppconst  33161  ressupprn  33162  mptctf  33187  orvcval2  34970  fineqvac  35642  fullfunfnv  36525  fullfunfv  36526  abrexdom  38480  diaf11N  41922  dibf11N  42034  imadomfi  42868  gneispace3  44973  fresfo  47936  funbrafvb  48044  funopafvb  48045  funbrafv22b  48138  funopafv2b  48139  dfclnbgr3  48742  grimuhgr  48803