Theorem funfn 6546

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 537	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6519	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 280	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1559  dom cdm 5643  Fun wfun 6510   Fn wfn 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-fn 6519

This theorem is referenced by:  funfnd  6547  funssxp  6715  funforn  6780  funbrfvb  6915  funopfvb  6916  ssimaex  6947  fvco  6960  fvco4i  6964  eqfunfv  7012  fvimacnvi  7028  unpreima  7039  respreima  7042  elrnrexdm  7065  elrnrexdmb  7066  ffvresb  7102  funiun  7124  funressn  7137  funresdfunsn  7168  funex  7198  elunirn  7230  suppval1  8140  funsssuppss  8164  smores  8317  rdgsucg  8388  rdglimg  8390  imafiOLD  9254  fundmfibi  9273  residfi  9275  mptfi  9288  ordtypelem6  9465  ordtypelem7  9466  harwdom  9533  ackbij2  10192  mptct  10489  smobeth  10538  hashkf  14339  hashfun  14444  fclim  15571  coapm  18095  psgnghm  21620  lindfrn  21861  elno3  27707  noextenddif  27720  noextendlt  27721  noextendgt  27722  nosupbnd2lem1  27767  noetasuplem4  27788  ausgrumgri  29325  dfnbgr3  29496  wlkiswwlks1  30024  vdn0conngrumgrv2  30355  hlimf  31397  adj1o  32054  abrexdomjm  32666  iunpreima  32724  fresf1o  32794  unipreima  32806  xppreima  32808  rnressnsn  32840  suppiniseg  32849  fdifsuppconst  32852  ressupprn  32853  mptctf  32879  orvcval2  34717  fineqvac  35373  fullfunfnv  36257  fullfunfv  36258  abrexdom  38190  diaf11N  41634  dibf11N  41746  imadomfi  42580  gneispace3  44670  fresfo  47603  funbrafvb  47711  funopafvb  47712  funbrafv22b  47805  funopafv2b  47806  dfclnbgr3  48409  grimuhgr  48470