Theorem funfn 6522

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 2740	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 534	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6495	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 279	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  dom cdm 5625  Fun wfun 6486   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-fn 6495

This theorem is referenced by:  funfnd  6523  funssxp  6690  funforn  6753  funbrfvb  6887  funopfvb  6888  ssimaex  6919  fvco  6932  fvco4i  6936  eqfunfv  6984  fvimacnvi  7000  unpreima  7011  respreima  7014  elrnrexdm  7037  elrnrexdmb  7038  ffvresb  7074  funiun  7096  funressn  7109  funresdfunsn  7140  funex  7170  elunirn  7202  suppval1  8113  funsssuppss  8137  smores  8289  rdgsucg  8359  rdglimg  8361  imafiOLD  9223  fundmfibi  9243  residfi  9245  mptfi  9258  ordtypelem6  9435  ordtypelem7  9436  harwdom  9503  ackbij2  10162  mptct  10458  smobeth  10507  hashkf  14292  hashfun  14397  fclim  15513  coapm  18036  psgnghm  21562  lindfrn  21803  elno3  27644  noextenddif  27657  noextendlt  27658  noextendgt  27659  nosupbnd2lem1  27704  noetasuplem4  27725  ausgrumgri  29261  dfnbgr3  29432  wlkiswwlks1  29960  vdn0conngrumgrv2  30291  hlimf  31333  adj1o  31990  abrexdomjm  32602  iunpreima  32660  fresf1o  32730  unipreima  32742  xppreima  32744  rnressnsn  32776  suppiniseg  32785  fdifsuppconst  32788  ressupprn  32789  mptctf  32815  orvcval2  34650  fineqvac  35304  fullfunfnv  36181  fullfunfv  36182  abrexdom  38104  diaf11N  41548  dibf11N  41660  imadomfi  42494  gneispace3  44584  fresfo  47518  funbrafvb  47626  funopafvb  47627  funbrafv22b  47720  funopafv2b  47721  dfclnbgr3  48324  grimuhgr  48385