Theorem funfn 5877

Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)

Assertion

Ref	Expression
funfn	⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Proof of Theorem funfn

Step	Hyp	Ref	Expression
1		eqid 2621	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 526	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5850	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 267	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1480  dom cdm 5074  Fun wfun 5841   Fn wfn 5842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-fn 5850

This theorem is referenced by:  funssxp  6018  funforn  6079  funbrfvb  6195  funopfvb  6196  ssimaex  6220  fvco  6231  fvco4i  6233  eqfunfv  6272  fvimacnvi  6287  unpreima  6297  respreima  6300  elrnrexdm  6319  elrnrexdmb  6320  ffvresb  6349  funiun  6366  funressn  6380  funresdfunsn  6409  resfunexg  6433  funex  6436  funiunfv  6460  elunirn  6463  suppval1  7246  funsssuppss  7266  wfrlem4  7363  smores  7394  smores2  7396  tfrlem1  7417  rdgsucg  7464  rdglimg  7466  fundmfibi  8189  resfnfinfin  8190  residfi  8191  mptfi  8209  resfifsupp  8247  ordtypelem4  8370  ordtypelem6  8372  ordtypelem7  8373  ordtypelem9  8375  ordtypelem10  8376  harwdom  8439  ackbij2  9009  brdom3  9294  brdom5  9295  brdom4  9296  mptct  9304  smobeth  9352  fpwwe2lem11  9406  hashkf  13059  hashfun  13164  hashimarn  13165  resunimafz0  13167  fclim  14218  isstruct2  15790  xpsc0  16141  xpsc1  16142  invf  16349  coapm  16642  psgnghm  19845  lindfrn  20079  ofco2  20176  dfac14  21331  perfdvf  23573  c1lip2  23665  taylf  24019  lpvtx  25859  upgrle2  25895  uhgrvtxedgiedgb  25926  ausgrumgri  25955  uhgr2edg  25993  ushgredgedg  26014  ushgredgedgloop  26016  subgruhgredgd  26069  subuhgr  26071  subupgr  26072  subumgr  26073  subusgr  26074  dfnbgr3  26123  vtxdun  26263  upgrewlkle2  26372  wlkiswwlks1  26622  vdn0conngrumgrv2  26922  eupthvdres  26961  hlimf  27943  adj1o  28602  abrexdomjm  29192  iunpreima  29228  fresf1o  29277  unipreima  29288  xppreima  29291  mptctf  29338  sitgf  30190  orvcval2  30301  frrlem4  31484  elno3  31509  noextenddif  31525  noextendlt  31526  noextendgt  31527  fullfunfnv  31695  fullfunfv  31696  abrexdom  33157  diaf11N  35818  dibf11N  35930  gneispace3  37913  gneispace  37914  gneispacef2  37916  funfnd  38905  funcoressn  40511  funbrafvb  40540  funopafvb  40541