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

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

Proof of Theorem ffn
StepHypRef Expression
1 df-f 5097 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simplbi 272 1 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 3041  ran crn 4510   Fn wfn 5088  wf 5089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-f 5097
This theorem is referenced by:  ffnd  5243  ffun  5245  frel  5247  fdm  5248  fresin  5271  fcoi1  5273  feu  5275  f0bi  5285  fnconstg  5290  f1fn  5300  fofn  5317  dffo2  5319  f1ofn  5336  feqmptd  5442  fvco3  5460  ffvelrn  5521  dff2  5532  dffo3  5535  dffo4  5536  dffo5  5537  f1ompt  5539  ffnfv  5546  fcompt  5558  fsn2  5562  fconst2g  5603  fconstfvm  5606  fex  5615  dff13  5637  cocan1  5656  off  5962  suppssof1  5967  ofco  5968  caofref  5971  caofrss  5974  caoftrn  5975  fo1stresm  6027  fo2ndresm  6028  1stcof  6029  2ndcof  6030  fo2ndf  6092  tposf2  6133  smoiso  6167  tfrcllemssrecs  6217  tfrcllemsucaccv  6219  elmapfn  6533  mapsn  6552  mapen  6708  updjudhcoinlf  6933  updjudhcoinrg  6934  updjud  6935  omp1eomlem  6947  dfz2  9091  uzn0  9309  unirnioo  9724  dfioo2  9725  ioorebasg  9726  fzen  9791  fseq1p1m1  9842  2ffzeq  9886  fvinim0ffz  9986  frecuzrdglem  10152  frecuzrdgtcl  10153  frecuzrdg0  10154  frecuzrdgfunlem  10160  frecuzrdg0t  10163  seq3val  10199  seqvalcd  10200  ser0f  10256  ffz0hash  10544  fnfzo0hash  10546  shftf  10570  uzin2  10727  rexanuz  10728  eff2  11313  reeff1  11334  tanvalap  11342  lmbr2  12310  cncnpi  12324  cncnp  12326  cnpdis  12338  lmff  12345  tx1cn  12365  tx2cn  12366  upxp  12368  txcnmpt  12369  uptx  12370  xmettpos  12466  blrnps  12507  blrn  12508  xmeterval  12531  qtopbasss  12617  cnbl0  12630  cnblcld  12631  tgioo  12642  tgqioo  12643  dvfre  12770  pilem1  12787  isomninnlem  13152  taupi  13166
  Copyright terms: Public domain W3C validator