Theorem funfn 6518

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 2733	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 529	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6491	. 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 5621  Fun wfun 6482   Fn wfn 6483

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 2123  ax-ext 2705

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

This theorem is referenced by:  funfnd  6519  funssxp  6686  funforn  6749  funbrfvb  6883  funopfvb  6884  ssimaex  6915  fvco  6928  fvco4i  6931  eqfunfv  6977  fvimacnvi  6993  unpreima  7004  respreima  7007  elrnrexdm  7030  elrnrexdmb  7031  ffvresb  7066  funiun  7088  funressn  7100  funresdfunsn  7131  funex  7161  elunirn  7193  suppval1  8104  funsssuppss  8128  smores  8280  rdgsucg  8350  rdglimg  8352  imafiOLD  9209  fundmfibi  9229  residfi  9231  mptfi  9244  ordtypelem6  9418  ordtypelem7  9419  harwdom  9486  ackbij2  10142  mptct  10438  smobeth  10486  hashkf  14243  hashfun  14348  fclim  15464  coapm  17982  psgnghm  21521  lindfrn  21762  elno3  27597  noextenddif  27610  noextendlt  27611  noextendgt  27612  nosupbnd2lem1  27657  noetasuplem4  27678  ausgrumgri  29149  dfnbgr3  29320  wlkiswwlks1  29849  vdn0conngrumgrv2  30180  hlimf  31221  adj1o  31878  abrexdomjm  32491  iunpreima  32548  fresf1o  32617  unipreima  32629  xppreima  32631  rnressnsn  32664  suppiniseg  32673  fdifsuppconst  32676  ressupprn  32677  mptctf  32705  orvcval2  34495  fineqvac  35162  fullfunfnv  36013  fullfunfv  36014  abrexdom  37793  diaf11N  41171  dibf11N  41283  imadomfi  42118  gneispace3  44253  fresfo  47175  funbrafvb  47283  funopafvb  47284  funbrafv22b  47377  funopafv2b  47378  dfclnbgr3  47953  grimuhgr  48014