ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ffn Structured version   GIF version

Theorem ffn 4989
Description: A mapping is a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
ffn (𝐹:AB𝐹 Fn A)

Proof of Theorem ffn
StepHypRef Expression
1 df-f 4849 . 2 (𝐹:AB ↔ (𝐹 Fn A ran 𝐹B))
21simplbi 259 1 (𝐹:AB𝐹 Fn A)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 2911  ran crn 4289   Fn wfn 4840  wf 4841
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-f 4849
This theorem is referenced by:  ffun  4991  frel  4992  fdm  4993  fresin  5011  fcoi1  5013  feu  5015  fnconstg  5027  f1fn  5036  fofn  5051  dffo2  5053  f1ofn  5070  feqmptd  5169  fvco3  5187  ffvelrn  5243  dff2  5254  dffo3  5257  dffo4  5258  dffo5  5259  f1ompt  5263  ffnfv  5266  fcompt  5276  fsn2  5280  fconst2g  5319  fconstfvm  5322  fex  5331  dff13  5350  cocan1  5370  off  5666  suppssof1  5670  ofco  5671  caofref  5674  caofrss  5677  caoftrn  5678  fo1stresm  5730  fo2ndresm  5731  1stcof  5732  2ndcof  5733  fo2ndf  5790  tposf2  5824  smoiso  5858  dfz2  8049  uzn0  8224  unirnioo  8572  dfioo2  8573  ioorebasg  8574  fzen  8637  fseq1p1m1  8686  2ffzeq  8728
  Copyright terms: Public domain W3C validator