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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  dom cdm 5624  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6495

This theorem is referenced by:  funfnd  6523  funssxp  6690  funforn  6753  funbrfvb  6887  funopfvb  6888  ssimaex  6919  fvco  6932  fvco4i  6935  eqfunfv  6982  fvimacnvi  6998  unpreima  7009  respreima  7012  elrnrexdm  7035  elrnrexdmb  7036  ffvresb  7072  funiun  7094  funressn  7106  funresdfunsn  7137  funex  7167  elunirn  7199  suppval1  8109  funsssuppss  8133  smores  8285  rdgsucg  8355  rdglimg  8357  imafiOLD  9219  fundmfibi  9239  residfi  9241  mptfi  9254  ordtypelem6  9431  ordtypelem7  9432  harwdom  9499  ackbij2  10155  mptct  10451  smobeth  10500  hashkf  14285  hashfun  14390  fclim  15506  coapm  18029  psgnghm  21570  lindfrn  21811  elno3  27633  noextenddif  27646  noextendlt  27647  noextendgt  27648  nosupbnd2lem1  27693  noetasuplem4  27714  ausgrumgri  29250  dfnbgr3  29421  wlkiswwlks1  29950  vdn0conngrumgrv2  30281  hlimf  31323  adj1o  31980  abrexdomjm  32592  iunpreima  32649  fresf1o  32719  unipreima  32731  xppreima  32733  rnressnsn  32765  suppiniseg  32774  fdifsuppconst  32777  ressupprn  32778  mptctf  32804  orvcval2  34619  fineqvac  35276  fullfunfnv  36144  fullfunfv  36145  abrexdom  38065  diaf11N  41509  dibf11N  41621  imadomfi  42455  gneispace3  44578  fresfo  47508  funbrafvb  47616  funopafvb  47617  funbrafv22b  47710  funopafv2b  47711  dfclnbgr3  48314  grimuhgr  48375