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

Theorem ffn 5272
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 5127 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simplbi 272 1 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 3071  ran crn 4540   Fn wfn 5118  wf 5119
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 5127
This theorem is referenced by:  ffnd  5273  ffun  5275  frel  5277  fdm  5278  fresin  5301  fcoi1  5303  feu  5305  f0bi  5315  fnconstg  5320  f1fn  5330  fofn  5347  dffo2  5349  f1ofn  5368  feqmptd  5474  fvco3  5492  ffvelrn  5553  dff2  5564  dffo3  5567  dffo4  5568  dffo5  5569  f1ompt  5571  ffnfv  5578  fcompt  5590  fsn2  5594  fconst2g  5635  fconstfvm  5638  fex  5647  dff13  5669  cocan1  5688  off  5994  suppssof1  5999  ofco  6000  caofref  6003  caofrss  6006  caoftrn  6007  fo1stresm  6059  fo2ndresm  6060  1stcof  6061  2ndcof  6062  fo2ndf  6124  tposf2  6165  smoiso  6199  tfrcllemssrecs  6249  tfrcllemsucaccv  6251  elmapfn  6565  mapsn  6584  mapen  6740  updjudhcoinlf  6965  updjudhcoinrg  6966  updjud  6967  omp1eomlem  6979  dfz2  9130  uzn0  9348  unirnioo  9763  dfioo2  9764  ioorebasg  9765  fzen  9830  fseq1p1m1  9881  2ffzeq  9925  fvinim0ffz  10025  frecuzrdglem  10191  frecuzrdgtcl  10192  frecuzrdg0  10193  frecuzrdgfunlem  10199  frecuzrdg0t  10202  seq3val  10238  seqvalcd  10239  ser0f  10295  ffz0hash  10583  fnfzo0hash  10585  shftf  10609  uzin2  10766  rexanuz  10767  prodf1f  11319  eff2  11393  reeff1  11414  tanvalap  11422  lmbr2  12393  cncnpi  12407  cncnp  12409  cnpdis  12421  lmff  12428  tx1cn  12448  tx2cn  12449  upxp  12451  txcnmpt  12452  uptx  12453  xmettpos  12549  blrnps  12590  blrn  12591  xmeterval  12614  qtopbasss  12700  cnbl0  12713  cnblcld  12714  tgioo  12725  tgqioo  12726  dvfre  12853  reeff1o  12872  pilem1  12873  ioocosf1o  12948  dfrelog  12952  isomninnlem  13255  taupi  13269
  Copyright terms: Public domain W3C validator