MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funfn Structured version   Visualization version   GIF version

Theorem funfn 6071
Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
Assertion
Ref Expression
funfn (Fun 𝐴𝐴 Fn dom 𝐴)

Proof of Theorem funfn
StepHypRef Expression
1 eqid 2752 . . 3 dom 𝐴 = dom 𝐴
21biantru 527 . 2 (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3 df-fn 6044 . 2 (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
42, 3bitr4i 267 1 (Fun 𝐴𝐴 Fn dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1624  dom cdm 5258  Fun wfun 6035   Fn wfn 6036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-cleq 2745  df-fn 6044
This theorem is referenced by:  funfnd  6072  funssxp  6214  funforn  6275  funbrfvb  6391  funopfvb  6392  ssimaex  6417  fvco  6428  fvco4i  6430  eqfunfv  6471  fvimacnvi  6486  unpreima  6496  respreima  6499  elrnrexdm  6518  elrnrexdmb  6519  ffvresb  6549  funiun  6567  funressn  6581  funresdfunsn  6611  resfunexg  6635  funex  6638  funiunfv  6661  elunirn  6664  suppval1  7461  funsssuppss  7482  wfrlem4  7579  smores  7610  smores2  7612  tfrlem1  7633  rdgsucg  7680  rdglimg  7682  fundmfibi  8402  resfnfinfin  8403  residfi  8404  mptfi  8422  resfifsupp  8460  ordtypelem4  8583  ordtypelem6  8585  ordtypelem7  8586  ordtypelem9  8588  ordtypelem10  8589  harwdom  8652  ackbij2  9249  brdom3  9534  brdom5  9535  brdom4  9536  mptct  9544  smobeth  9592  fpwwe2lem11  9646  hashkf  13305  hashfun  13408  hashimarn  13411  resunimafz0  13413  fclim  14475  isstruct2  16061  xpsc0  16414  xpsc1  16415  invf  16621  coapm  16914  psgnghm  20120  lindfrn  20354  ofco2  20451  dfac14  21615  perfdvf  23858  c1lip2  23952  taylf  24306  lpvtx  26154  upgrle2  26191  uhgrvtxedgiedgb  26222  ausgrumgri  26253  uhgr2edg  26291  ushgredgedg  26312  ushgredgedgloop  26314  subgruhgredgd  26367  subuhgr  26369  subupgr  26370  subumgr  26371  subusgr  26372  dfnbgr3  26422  vtxdun  26579  upgrewlkle2  26704  wlkiswwlks1  26968  vdn0conngrumgrv2  27340  eupthvdres  27379  hlimf  28395  adj1o  29054  abrexdomjm  29644  iunpreima  29682  fresf1o  29734  unipreima  29747  xppreima  29750  mptctf  29796  sitgf  30710  orvcval2  30821  frrlem4  32081  elno3  32106  noextenddif  32119  noextendlt  32120  noextendgt  32121  nosupbnd2lem1  32159  noetalem3  32163  fullfunfnv  32351  fullfunfv  32352  abrexdom  33830  diaf11N  36832  dibf11N  36944  gneispace3  38925  gneispace  38926  gneispacef2  38928  funcoressn  41705  funbrafvb  41734  funopafvb  41735
  Copyright terms: Public domain W3C validator