Theorem funfn 6131

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 2806	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 521	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6104	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 269	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 197   ∧ wa 384   = wceq 1637  dom cdm 5311  Fun wfun 6095   Fn wfn 6096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-fn 6104

This theorem is referenced by:  funfnd  6132  funssxp  6276  funforn  6338  funbrfvb  6458  funopfvb  6459  ssimaex  6484  fvco  6495  fvco4i  6497  eqfunfv  6538  fvimacnvi  6553  unpreima  6563  respreima  6566  elrnrexdm  6585  elrnrexdmb  6586  ffvresb  6616  funiun  6636  funressn  6650  funresdfunsn  6680  resfunexg  6704  funex  6707  funiunfv  6730  elunirn  6733  suppval1  7535  funsssuppss  7556  wfrlem4OLD  7654  smores  7685  smores2  7687  tfrlem1  7708  rdgsucg  7755  rdglimg  7757  fundmfibi  8484  resfnfinfin  8485  residfi  8486  mptfi  8504  resfifsupp  8542  ordtypelem4  8665  ordtypelem6  8667  ordtypelem7  8668  ordtypelem9  8670  ordtypelem10  8671  harwdom  8734  ackbij2  9350  brdom3  9635  brdom5  9636  brdom4  9637  mptct  9645  smobeth  9693  fpwwe2lem11  9747  hashkf  13339  hashfun  13441  hashimarn  13444  resunimafz0  13446  fclim  14507  isstruct2  16078  xpsc0  16425  xpsc1  16426  invf  16632  coapm  16925  psgnghm  20133  lindfrn  20370  ofco2  20468  dfac14  21635  perfdvf  23881  c1lip2  23975  taylf  24329  lpvtx  26177  upgrle2  26214  uhgrvtxedgiedgbOLD  26246  ausgrumgri  26277  uhgr2edg  26315  ushgredgedg  26336  ushgredgedgloopOLD  26339  subgruhgredgd  26392  subuhgr  26394  subupgr  26395  subumgr  26396  subusgr  26397  dfnbgr3  26447  vtxdun  26605  upgrewlkle2  26730  wlkiswwlks1  26994  vdn0conngrumgrv2  27369  eupthvdres  27408  hlimf  28422  adj1o  29081  abrexdomjm  29670  iunpreima  29708  fresf1o  29760  unipreima  29773  xppreima  29776  mptctf  29822  sitgf  30734  orvcval2  30845  frrlem4  32104  elno3  32129  noextenddif  32142  noextendlt  32143  noextendgt  32144  nosupbnd2lem1  32182  noetalem3  32186  fullfunfnv  32374  fullfunfv  32375  abrexdom  33837  diaf11N  36830  dibf11N  36942  gneispace3  38931  gneispace  38932  gneispacef2  38934  funcoressn  41661  funbrafvb  41745  funopafvb  41746  funbrafv22b  41839  funopafv2b  41840