Theorem funfn 6568

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 2761	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 539	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6540	. 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 5651  Fun wfun 6531   Fn wfn 6532

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 2733

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

This theorem is used by:  funfnd  6569  funssxp  6736  funforn  6801  funbrfvb  6936  funopfvb  6937  ssimaex  6968  fvco  6981  fvco4i  6985  eqfunfv  7033  fvimacnvi  7049  unpreima  7060  respreima  7063  iunpreima  7066  elrnrexdm  7087  elrnrexdmb  7088  ffvresb  7124  funiun  7148  funressn  7161  funresdfunsn  7192  funex  7223  elunirn  7253  suppval1  8176  funsssuppss  8200  smores  8353  rdgsucg  8424  rdglimg  8426  fundmfibi  9318  residfi  9320  mptfi  9333  ordtypelem6  9510  ordtypelem7  9511  harwdom  9578  ackbij2  10313  imadomnum  10607  mptct  10615  smobeth  10664  hashkf  14469  hashfun  14575  fclim  15713  coapm  18239  psgnghm  21879  lindfrn  22120  elno3  28005  noextenddif  28018  noextendlt  28019  noextendgt  28020  nosupbnd2lem1  28065  noetasuplem4  28086  ausgrumgri  29741  dfnbgr3  29912  wlkiswwlks1  30449  vdn0conngrumgrv2  30790  hlimf  31832  adj1o  32489  abrexdomjm  33096  fresf1o  33218  unipreima  33230  xppreima  33232  rnressnsn  33264  suppiniseg  33272  fdifsuppconst  33275  ressupprn  33276  mptctf  33301  orvcval2  35084  fineqvac  35767  fullfunfnv  36690  fullfunfv  36691  abrexdom  38644  diaf11N  42086  dibf11N  42198  imadomfi  43032  gneispace3  45118  fresfo  48087  funbrafvb  48195  funopafvb  48196  funbrafv22b  48289  funopafv2b  48290  dfclnbgr3  48893  grimuhgr  48954