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

Theorem ffn 5318
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 5173 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simplbi 272 1 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 3102  ran crn 4586   Fn wfn 5164  wf 5165
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 5173
This theorem is referenced by:  ffnd  5319  ffun  5321  frel  5323  fdm  5324  fresin  5347  fcoi1  5349  feu  5351  f0bi  5361  fnconstg  5366  f1fn  5376  fofn  5393  dffo2  5395  f1ofn  5414  feqmptd  5520  fvco3  5538  ffvelrn  5599  dff2  5610  dffo3  5613  dffo4  5614  dffo5  5615  f1ompt  5617  ffnfv  5624  fcompt  5636  fsn2  5640  fconst2g  5681  fconstfvm  5684  fex  5693  dff13  5715  cocan1  5734  off  6041  suppssof1  6046  ofco  6047  caofref  6050  caofrss  6053  caoftrn  6054  fo1stresm  6106  fo2ndresm  6107  1stcof  6108  2ndcof  6109  fo2ndf  6171  tposf2  6212  smoiso  6246  tfrcllemssrecs  6296  tfrcllemsucaccv  6298  elmapfn  6613  mapsn  6632  mapen  6788  updjudhcoinlf  7019  updjudhcoinrg  7020  updjud  7021  omp1eomlem  7033  dfz2  9231  uzn0  9449  unirnioo  9872  dfioo2  9873  ioorebasg  9874  fzen  9940  fseq1p1m1  9991  2ffzeq  10035  fvinim0ffz  10135  frecuzrdglem  10305  frecuzrdgtcl  10306  frecuzrdg0  10307  frecuzrdgfunlem  10313  frecuzrdg0t  10316  seq3val  10352  seqvalcd  10353  ser0f  10409  ffz0hash  10699  fnfzo0hash  10701  shftf  10725  uzin2  10882  rexanuz  10883  prodf1f  11435  eff2  11572  reeff1  11592  tanvalap  11600  lmbr2  12601  cncnpi  12615  cncnp  12617  cnpdis  12629  lmff  12636  tx1cn  12656  tx2cn  12657  upxp  12659  txcnmpt  12660  uptx  12661  xmettpos  12757  blrnps  12798  blrn  12799  xmeterval  12822  qtopbasss  12908  cnbl0  12921  cnblcld  12922  tgioo  12933  tgqioo  12934  dvfre  13061  reeff1o  13081  pilem1  13087  ioocosf1o  13162  dfrelog  13168  012of  13554  2o01f  13555  taupi  13628
  Copyright terms: Public domain W3C validator