Theorem funfn 6410

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

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1543  dom cdm 5551  Fun wfun 6374   Fn wfn 6375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729  df-fn 6383

This theorem is referenced by:  funfnd  6411  funssxp  6574  funforn  6640  funbrfvb  6767  funopfvb  6768  ssimaex  6796  fvco  6809  fvco4i  6812  eqfunfv  6857  fvimacnvi  6872  unpreima  6883  respreima  6886  elrnrexdm  6908  elrnrexdmb  6909  ffvresb  6941  funiun  6962  funressn  6974  funresdfunsn  7004  funex  7035  elunirn  7064  suppval1  7909  funsssuppss  7932  smores  8089  rdgsucg  8159  rdglimg  8161  imafi  8853  fundmfibi  8955  residfi  8957  mptfi  8975  ordtypelem6  9139  ordtypelem7  9140  harwdom  9207  ackbij2  9857  mptct  10152  smobeth  10200  hashkf  13898  hashfun  14004  fclim  15114  coapm  17577  psgnghm  20542  lindfrn  20783  ausgrumgri  27258  dfnbgr3  27426  wlkiswwlks1  27951  vdn0conngrumgrv2  28279  hlimf  29318  adj1o  29975  abrexdomjm  30571  iunpreima  30623  fresf1o  30685  unipreima  30700  xppreima  30702  suppiniseg  30740  fdifsuppconst  30743  ressupprn  30744  mptctf  30772  orvcval2  32137  fineqvac  32779  elno3  33595  noextenddif  33608  noextendlt  33609  noextendgt  33610  nosupbnd2lem1  33655  noetasuplem4  33676  fullfunfnv  33985  fullfunfv  33986  abrexdom  35625  diaf11N  38800  dibf11N  38912  gneispace3  41420  fresfo  44214  funbrafvb  44320  funopafvb  44321  funbrafv22b  44414  funopafv2b  44415