Theorem funfn 6570

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 2765	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 539	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6543	. 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 5663  Fun wfun 6534   Fn wfn 6535

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 2156  ax-ext 2737

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

This theorem is used by:  funfnd  6571  funssxp  6738  funforn  6803  funbrfvb  6938  funopfvb  6939  ssimaex  6970  fvco  6983  fvco4i  6987  eqfunfv  7035  fvimacnvi  7051  unpreima  7062  respreima  7065  elrnrexdm  7088  elrnrexdmb  7089  ffvresb  7125  funiun  7147  funressn  7160  funresdfunsn  7191  funex  7221  elunirn  7251  suppval1  8164  funsssuppss  8188  smores  8341  rdgsucg  8412  rdglimg  8414  fundmfibi  9296  residfi  9298  mptfi  9311  ordtypelem6  9488  ordtypelem7  9489  harwdom  9556  ackbij2  10237  mptct  10533  smobeth  10582  hashkf  14381  hashfun  14487  fclim  15623  coapm  18145  psgnghm  21759  lindfrn  22000  elno3  27848  noextenddif  27861  noextendlt  27862  noextendgt  27863  nosupbnd2lem1  27908  noetasuplem4  27929  ausgrumgri  29546  dfnbgr3  29717  wlkiswwlks1  30245  vdn0conngrumgrv2  30576  hlimf  31618  adj1o  32275  abrexdomjm  32882  iunpreima  32938  fresf1o  33005  unipreima  33017  xppreima  33019  rnressnsn  33051  suppiniseg  33060  fdifsuppconst  33063  ressupprn  33064  mptctf  33090  orvcval2  34873  fineqvac  35545  fullfunfnv  36451  fullfunfv  36452  abrexdom  38414  diaf11N  41856  dibf11N  41968  imadomfi  42802  gneispace3  44892  fresfo  47818  funbrafvb  47926  funopafvb  47927  funbrafv22b  48020  funopafv2b  48021  dfclnbgr3  48624  grimuhgr  48685