Theorem funfn 6079

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 2760	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 527	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6052	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 267	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 196   ∧ wa 383   = wceq 1632  dom cdm 5266  Fun wfun 6043   Fn wfn 6044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-fn 6052

This theorem is referenced by:  funfnd  6080  funssxp  6222  funforn  6284  funbrfvb  6400  funopfvb  6401  ssimaex  6426  fvco  6437  fvco4i  6439  eqfunfv  6480  fvimacnvi  6495  unpreima  6505  respreima  6508  elrnrexdm  6527  elrnrexdmb  6528  ffvresb  6558  funiun  6576  funressn  6590  funresdfunsn  6620  resfunexg  6644  funex  6647  funiunfv  6670  elunirn  6673  suppval1  7470  funsssuppss  7491  wfrlem4  7588  smores  7619  smores2  7621  tfrlem1  7642  rdgsucg  7689  rdglimg  7691  fundmfibi  8412  resfnfinfin  8413  residfi  8414  mptfi  8432  resfifsupp  8470  ordtypelem4  8593  ordtypelem6  8595  ordtypelem7  8596  ordtypelem9  8598  ordtypelem10  8599  harwdom  8662  ackbij2  9277  brdom3  9562  brdom5  9563  brdom4  9564  mptct  9572  smobeth  9620  fpwwe2lem11  9674  hashkf  13333  hashfun  13436  hashimarn  13439  resunimafz0  13441  fclim  14503  isstruct2  16089  xpsc0  16442  xpsc1  16443  invf  16649  coapm  16942  psgnghm  20148  lindfrn  20382  ofco2  20479  dfac14  21643  perfdvf  23886  c1lip2  23980  taylf  24334  lpvtx  26183  upgrle2  26220  uhgrvtxedgiedgb  26251  ausgrumgri  26282  uhgr2edg  26320  ushgredgedg  26341  ushgredgedgloop  26343  subgruhgredgd  26396  subuhgr  26398  subupgr  26399  subumgr  26400  subusgr  26401  dfnbgr3  26451  vtxdun  26608  upgrewlkle2  26733  wlkiswwlks1  26997  vdn0conngrumgrv2  27369  eupthvdres  27408  hlimf  28424  adj1o  29083  abrexdomjm  29673  iunpreima  29711  fresf1o  29763  unipreima  29776  xppreima  29779  mptctf  29825  sitgf  30739  orvcval2  30850  frrlem4  32110  elno3  32135  noextenddif  32148  noextendlt  32149  noextendgt  32150  nosupbnd2lem1  32188  noetalem3  32192  fullfunfnv  32380  fullfunfv  32381  abrexdom  33856  diaf11N  36858  dibf11N  36970  gneispace3  38951  gneispace  38952  gneispacef2  38954  funcoressn  41731  funbrafvb  41760  funopafvb  41761