Theorem funfn 6255

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 2795	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 530	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6228	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 279	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1522  dom cdm 5443  Fun wfun 6219   Fn wfn 6220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-fn 6228

This theorem is referenced by:  funfnd  6256  funssxp  6403  funforn  6465  funbrfvb  6588  funopfvb  6589  ssimaex  6615  fvco  6626  fvco4i  6629  eqfunfv  6672  fvimacnvi  6687  unpreima  6698  respreima  6701  elrnrexdm  6720  elrnrexdmb  6721  ffvresb  6751  funiun  6772  funressn  6784  funresdfunsn  6818  funex  6848  elunirn  6875  suppval1  7687  funsssuppss  7707  wfrlem4OLD  7810  smores  7841  rdgsucg  7911  rdglimg  7913  fundmfibi  8649  residfi  8651  mptfi  8669  ordtypelem6  8833  ordtypelem7  8834  harwdom  8900  ackbij2  9511  mptct  9806  smobeth  9854  hashkf  13542  hashfun  13646  fclim  14744  coapm  17160  psgnghm  20406  lindfrn  20647  ausgrumgri  26635  dfnbgr3  26803  wlkiswwlks1  27332  vdn0conngrumgrv2  27662  hlimf  28705  adj1o  29362  abrexdomjm  29959  iunpreima  30006  fresf1o  30066  unipreima  30081  xppreima  30084  mptctf  30141  orvcval2  31333  elno3  32772  noextenddif  32785  noextendlt  32786  noextendgt  32787  nosupbnd2lem1  32825  noetalem3  32829  fullfunfnv  33017  fullfunfv  33018  abrexdom  34556  diaf11N  37735  dibf11N  37847  gneispace3  39987  funbrafvb  42891  funopafvb  42892  funbrafv22b  42985  funopafv2b  42986