Theorem funfn 6387

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537  dom cdm 5557  Fun wfun 6351   Fn wfn 6352

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 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-fn 6360

This theorem is referenced by:  funfnd  6388  funssxp  6537  funforn  6599  funbrfvb  6722  funopfvb  6723  ssimaex  6750  fvco  6761  fvco4i  6764  eqfunfv  6809  fvimacnvi  6824  unpreima  6835  respreima  6838  elrnrexdm  6857  elrnrexdmb  6858  ffvresb  6890  funiun  6911  funressn  6923  funresdfunsn  6953  funex  6984  elunirn  7012  suppval1  7838  funsssuppss  7858  smores  7991  rdgsucg  8061  rdglimg  8063  fundmfibi  8805  residfi  8807  mptfi  8825  ordtypelem6  8989  ordtypelem7  8990  harwdom  9056  ackbij2  9667  mptct  9962  smobeth  10010  hashkf  13695  hashfun  13801  fclim  14912  coapm  17333  psgnghm  20726  lindfrn  20967  ausgrumgri  26954  dfnbgr3  27122  wlkiswwlks1  27647  vdn0conngrumgrv2  27977  hlimf  29016  adj1o  29673  abrexdomjm  30269  iunpreima  30318  fresf1o  30378  unipreima  30393  xppreima  30396  mptctf  30455  orvcval2  31718  elno3  33164  noextenddif  33177  noextendlt  33178  noextendgt  33179  nosupbnd2lem1  33217  noetalem3  33221  fullfunfnv  33409  fullfunfv  33410  abrexdom  35007  diaf11N  38187  dibf11N  38299  gneispace3  40490  funbrafvb  43362  funopafvb  43363  funbrafv22b  43456  funopafv2b  43457