Theorem funfn 5918

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

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1483  dom cdm 5114  Fun wfun 5882   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-fn 5891

This theorem is referenced by:  funfnd  5919  funssxp  6061  funforn  6122  funbrfvb  6238  funopfvb  6239  ssimaex  6263  fvco  6274  fvco4i  6276  eqfunfv  6316  fvimacnvi  6331  unpreima  6341  respreima  6344  elrnrexdm  6363  elrnrexdmb  6364  ffvresb  6394  funiun  6412  funressn  6426  funresdfunsn  6455  resfunexg  6479  funex  6482  funiunfv  6506  elunirn  6509  suppval1  7301  funsssuppss  7321  wfrlem4  7418  smores  7449  smores2  7451  tfrlem1  7472  rdgsucg  7519  rdglimg  7521  fundmfibi  8245  resfnfinfin  8246  residfi  8247  mptfi  8265  resfifsupp  8303  ordtypelem4  8426  ordtypelem6  8428  ordtypelem7  8429  ordtypelem9  8431  ordtypelem10  8432  harwdom  8495  ackbij2  9065  brdom3  9350  brdom5  9351  brdom4  9352  mptct  9360  smobeth  9408  fpwwe2lem11  9462  hashkf  13119  hashfun  13224  hashimarn  13227  resunimafz0  13229  fclim  14284  isstruct2  15867  xpsc0  16220  xpsc1  16221  invf  16428  coapm  16721  psgnghm  19926  lindfrn  20160  ofco2  20257  dfac14  21421  perfdvf  23667  c1lip2  23761  taylf  24115  lpvtx  25963  upgrle2  26000  uhgrvtxedgiedgb  26031  ausgrumgri  26062  uhgr2edg  26100  ushgredgedg  26121  ushgredgedgloop  26123  subgruhgredgd  26176  subuhgr  26178  subupgr  26179  subumgr  26180  subusgr  26181  dfnbgr3  26236  vtxdun  26377  upgrewlkle2  26502  wlkiswwlks1  26753  vdn0conngrumgrv2  27056  eupthvdres  27095  hlimf  28094  adj1o  28753  abrexdomjm  29345  iunpreima  29383  fresf1o  29433  unipreima  29446  xppreima  29449  mptctf  29495  sitgf  30409  orvcval2  30520  frrlem4  31783  elno3  31808  noextenddif  31821  noextendlt  31822  noextendgt  31823  nosupbnd2lem1  31861  noetalem3  31865  fullfunfnv  32053  fullfunfv  32054  abrexdom  33525  diaf11N  36338  dibf11N  36450  gneispace3  38431  gneispace  38432  gneispacef2  38434  funcoressn  41207  funbrafvb  41236  funopafvb  41237