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 2769	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 538	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6536	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 281	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567  dom cdm 5659  Fun wfun 6527   Fn wfn 6528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-fn 6536

This theorem is referenced by:  funfnd  6564  funssxp  6732  funforn  6797  funbrfvb  6932  funopfvb  6933  ssimaex  6964  fvco  6977  fvco4i  6981  eqfunfv  7029  fvimacnvi  7045  unpreima  7056  respreima  7059  elrnrexdm  7082  elrnrexdmb  7083  ffvresb  7119  funiun  7141  funressn  7154  funresdfunsn  7185  funex  7215  elunirn  7247  suppval1  8158  funsssuppss  8182  smores  8335  rdgsucg  8406  rdglimg  8408  fundmfibi  9289  residfi  9291  mptfi  9304  ordtypelem6  9481  ordtypelem7  9482  harwdom  9549  ackbij2  10221  mptct  10518  smobeth  10567  hashkf  14364  hashfun  14470  fclim  15600  coapm  18124  psgnghm  21695  lindfrn  21936  elno3  27781  noextenddif  27794  noextendlt  27795  noextendgt  27796  nosupbnd2lem1  27841  noetasuplem4  27862  ausgrumgri  29454  dfnbgr3  29625  wlkiswwlks1  30153  vdn0conngrumgrv2  30484  hlimf  31526  adj1o  32183  abrexdomjm  32790  iunpreima  32846  fresf1o  32913  unipreima  32925  xppreima  32927  rnressnsn  32959  suppiniseg  32968  fdifsuppconst  32971  ressupprn  32972  mptctf  32998  orvcval2  34790  fineqvac  35448  fullfunfnv  36333  fullfunfv  36334  abrexdom  38264  diaf11N  41708  dibf11N  41820  imadomfi  42654  gneispace3  44744  fresfo  47667  funbrafvb  47775  funopafvb  47776  funbrafv22b  47869  funopafv2b  47870  dfclnbgr3  48473  grimuhgr  48534