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

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

Proof of Theorem ffn
StepHypRef Expression
1 df-f 6353 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simplbi 498 1 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3935  ran crn 5550   Fn wfn 6344  wf 6345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208  df-an 397  df-f 6353
This theorem is referenced by:  ffnd  6509  ffun  6511  frel  6513  fdm  6516  ffrn  6520  fresin  6541  fresaun  6543  fresaunres2  6544  fcoi1  6546  feu  6548  f0bi  6556  dffo2  6588  fimadmfo  6593  feqmptdf  6729  fvco3  6754  ffvelrn  6842  dff2  6858  dffo3  6861  dffo4  6862  dffo5  6863  f1ompt  6868  ffnfv  6875  frnssb  6878  fcompt  6888  fsn2  6891  fprb  6949  fconst2g  6958  fpr2g  6966  fex  6981  dff13  7004  nvocnv  7029  soisores  7069  fo1stres  7706  fo2ndres  7707  1stcof  7710  2ndcof  7711  curry1f  7792  curry2f  7794  fparlem1  7798  fparlem2  7799  fo2ndf  7808  tposf2  7907  smo11  7992  mapsnd  8439  pw2f1olem  8610  mapen  8670  mapunen  8675  fissuni  8818  fipreima  8819  indexfi  8821  mapfien  8860  oismo  8993  cantnflt  9124  cantnfp1lem3  9132  cantnflem4  9144  tcrank  9302  updjudhcoinlf  9350  updjudhcoinrg  9351  updjud  9352  infpwfien  9477  cardinfima  9512  dfacacn  9556  cfflb  9670  cofsmo  9680  cfcoflem  9683  coftr  9684  fin23lem40  9762  axdc3lem2  9862  ac6num  9890  ac6c4  9892  ac6s2  9897  ttukeylem6  9925  iunfo  9950  pwcfsdom  9994  fpwwe2lem6  10046  fpwwe2lem8  10048  pwfseqlem3  10071  inar1  10186  tskcard  10192  tskuni  10194  tskurn  10200  gruima  10213  nqerrel  10343  recmulnq  10375  dmrecnq  10379  axpre-sup  10580  ofsubeq0  11624  dfz2  11989  uzn0  12249  rpnnen1lem3  12368  rpnnen1lem5  12370  unirnioo  12827  dfioo2  12828  ioorebas  12829  fseq1p1m1  12971  2ffzeq  13018  fvinim0ffz  13146  injresinjlem  13147  fsequb2  13334  fseqsupcl  13335  fseqsupubi  13336  ser0f  13413  hashgval  13683  hashinf  13685  hashresfn  13690  ffz0hash  13795  fnfzo0hash  13798  wrdred1hash  13903  revlen  14114  revrev  14119  repswlen  14128  repsdf2  14130  cshword  14143  0csh0  14145  lenco  14184  s1co  14185  cshco  14188  swrdco  14189  ofccat  14319  shftf  14428  uzin2  14694  rexanuz  14695  limsuple  14825  limsupval2  14827  rlimres  14905  lo1res  14906  rlimresb  14912  isercolllem2  15012  isercolllem3  15013  isercoll  15014  supcvg  15201  prodf1f  15238  eff2  15442  reeff1  15463  tanval  15471  ruclem4  15577  ruclem12  15584  prmreclem6  16247  1arithlem4  16252  1arith  16253  vdwmc  16304  vdwlem1  16307  vdwlem8  16314  vdwlem13  16319  ramval  16334  0ram  16346  0ram2  16347  0ramcl  16349  ramcl  16355  fsets  16506  firest  16696  0ssc  17097  0subcat  17098  isfull2  17171  arwhoma  17295  gsumval2a  17885  isgrpinv  18096  f1omvdconj  18505  pmtrmvd  18515  pmtrfinv  18520  pmtrdifellem4  18538  efgsfo  18796  efgredlem  18804  efgcpbllemb  18812  frgpup3lem  18834  0frgp  18836  gexex  18904  torsubg  18905  gsumval3  18958  gsumzres  18960  gsummptmhm  18991  gsumzoppg  18995  dprdf1o  19085  dprd2db  19096  kerf1ghm  19428  kerf1hrmOLD  19429  srngf1o  19556  lmhmima  19750  lmhmpreima  19751  lmhmrnlss  19753  lspextmo  19759  pwssplit1  19762  psrbaglefi  20082  psrlidm  20113  mplmonmul  20175  evlseu  20226  mpfconst  20244  mpfproj  20245  mpfsubrg  20246  coe1sclmulfv  20381  pf1const  20439  pf1id  20440  pf1subrg  20441  mpfpf1  20444  pf1mpf  20445  cnfldplusf  20502  cnfldsub  20503  chrrhm  20608  znunit  20640  psgnevpmb  20661  psgndiflemB  20674  mpofrlmd  20851  frlmipval  20853  frlmphl  20855  frlmlbs  20871  frlmup4  20875  ellspd  20876  lindfmm  20901  lsslindf  20904  mamuass  20941  mamudi  20942  mamudir  20943  mamuvs1  20944  mamuvs2  20945  1mavmul  21087  mavmulass  21088  mdetunilem7  21157  madutpos  21181  lecldbas  21757  lmbr2  21797  cncnpi  21816  cncnp  21818  cnpdis  21831  lmff  21839  pnrmopn  21881  dnsconst  21916  cmpsub  21938  tgcmp  21939  hauscmplem  21944  2ndcctbss  21993  2ndcomap  21996  2ndcsep  21997  1stccnp  22000  kgenidm  22085  iskgen2  22086  1stckgen  22092  kgen2cn  22097  ptpjpre1  22109  pttop  22120  ptuni  22132  ptval2  22139  tx1cn  22147  tx2cn  22148  ptpjcn  22149  ptpjopn  22150  ptclsg  22153  ptcnplem  22159  upxp  22161  txcnmpt  22162  uptx  22163  txcmplem2  22180  txkgen  22190  xkoptsub  22192  xkopt  22193  xkococnlem  22197  xkococn  22198  ptcmpfi  22351  zfbas  22434  uzrest  22435  rnelfmlem  22490  rnelfm  22491  fmfnfmlem2  22493  fmfnfm  22496  lmflf  22543  alexsubALT  22589  clssubg  22646  qustgplem  22658  tsmsres  22681  tsmsxplem1  22690  ucncn  22823  xmettpos  22888  imasdsf1olem  22912  blrnps  22947  blrn  22948  xmeterval  22971  tmslem  23021  tmsxms  23025  imasf1oxms  23028  prdsxms  23069  blval2  23101  metuel2  23104  isngp2  23135  isngp3  23136  tngngp2  23190  isnghm  23261  qtopbaslem  23296  qdensere  23307  cnbl0  23311  cnblcld  23312  cnfldms  23313  blssioo  23332  tgioo  23333  tgqioo  23337  xrtgioo  23343  xrsdsre  23347  xrge0tsms  23371  iimulcn  23471  bndth  23491  lebnumlem3  23496  nmhmcn  23653  cphsqrtcl  23717  lmmbr2  23791  caucfil  23815  causs  23830  lmcau  23845  bcth3  23863  cncms  23887  cnfldcusp  23889  rrxmvallem  23936  ivthicc  23988  ovolfioo  23997  ovolficc  23998  ovolficcss  23999  ovollb2lem  24018  ovoliunlem2  24033  ovolshftlem1  24039  ovolicc2  24052  ismbl  24056  voliunlem2  24081  volsup  24086  ioorf  24103  ioorinv  24106  ioorcl  24107  uniiccdif  24108  uniioovol  24109  uniiccvol  24110  uniioombllem2  24113  uniioombllem4  24116  dyaddisj  24126  dyadmax  24128  dyadmbllem  24129  dyadmbl  24130  opnmbllem  24131  opnmblALT  24133  volsup2  24135  mbfdm  24156  mbfima  24160  mbfid  24165  ismbfd  24169  mbfres2  24175  mbfposr  24182  mbfimaopnlem  24185  mbflimsup  24196  0plef  24202  i1f1lem  24219  itg11  24221  itg1addlem4  24229  i1fpos  24236  itg1le  24243  itg1climres  24244  mbfi1fseqlem5  24249  mbfi1flimlem  24252  xrge0f  24261  itg2ge0  24265  itg2seq  24272  itg2i1fseqle  24284  itg2i1fseq2  24286  itg2addlem  24288  itg2gt0  24290  limciun  24421  dvres  24438  dvres3a  24441  cpnres  24463  dvfre  24477  dvmptres3  24482  dvlip2  24521  dvgt0lem2  24529  deg1fvi  24608  uc1pmon1p  24674  fta1g  24690  ig1peu  24694  ig1pdvds  24699  plyco0  24711  plypf1  24731  dgrlem  24748  dgrub  24753  dgrlb  24755  coemulc  24774  plyreres  24801  plydivlem3  24813  plydivlem4  24814  plydiveu  24816  plyremlem  24822  fta1lem  24825  fta1  24826  vieta1lem2  24829  plyexmo  24831  elaa  24834  elqaalem3  24839  aannenlem1  24846  pserulm  24939  psercnlem2  24941  psercnlem1  24942  psercn  24943  abelth  24958  reeff1o  24964  pilem1  24968  recosf1o  25046  resinf1o  25047  efif1olem3  25055  efif1olem4  25056  efifo  25058  eff1olem  25059  ellogrn  25070  logcn  25157  dvloglem  25158  logf1o2  25160  efopnlem1  25166  efopnlem2  25167  efopn  25168  logtayl  25170  cxpcn3lem  25255  cxpcn3  25256  resqrtcn  25257  asinneg  25391  areambl  25464  emcllem7  25507  lgamgulm2  25541  basellem4  25589  sqff1o  25687  dvdsmulf1o  25699  fsumdvdsmul  25700  ostthlem1  26131  ostth  26143  tglnfn  26261  f1otrg  26585  axlowdimlem6  26661  axlowdimlem8  26663  axlowdimlem9  26664  axlowdimlem11  26666  axlowdimlem12  26667  axlowdimlem17  26672  elntg2  26699  crctcshlem4  27526  clwlkclwwlklem2  27706  eucrct2eupth  27952  ex-fpar  28169  cnnvm  28387  sspmlem  28437  nvo00  28466  nmlno0lem  28498  phoeqi  28562  ubthlem1  28575  hhip  28882  hhssabloilem  28966  hhssnv  28969  hhsssh  28974  occllem  29008  shsel  29019  chscllem2  29343  df0op2  29457  hoeq  29465  hocofni  29472  hoaddfni  29475  hosubfni  29476  hon0  29498  ho01i  29533  hoeq1  29535  elnlfn  29633  nmlnop0iALT  29700  lnopco0i  29709  imaelshi  29763  nlelchi  29766  rnbra  29812  cnvbraval  29815  kbass5  29825  hmopidmchi  29856  hmopidmpji  29857  foresf1o  30193  fimarab  30319  fcomptf  30332  ofpreima  30339  resf1o  30393  maprnin  30394  fpwrelmapffslem  30395  hashgt1  30457  s3clhash  30552  xrge0tsmsd  30620  tocyc01  30688  cyc3evpm  30720  cycpmgcl  30723  cycpmconjslem2  30725  cyc3conja  30727  kerunit  30824  dimval  30901  dimvalfi  30902  txomap  30998  locfinreflem  31004  hauseqcn  31038  xpinpreima  31049  xpinpreima2  31050  tpr2rico  31055  mndpluscn  31069  rmulccn  31071  raddcn  31072  xrge0pluscn  31083  xrge0tmdALT  31089  rge0scvg  31092  pl1cn  31098  elzrhunit  31120  qqhf  31127  cnrrext  31151  qqhre  31161  indpi1  31179  indpreima  31184  1stmbfm  31418  2ndmbfm  31419  mbfmcnt  31426  omssubadd  31458  carsggect  31476  eulerpartlemsv2  31516  eulerpartlems  31518  eulerpartlemv  31522  eulerpartlemb  31526  eulerpartlemf  31528  eulerpartlemt  31529  eulerpartlemmf  31533  eulerpartlemgvv  31534  eulerpartlemgh  31536  eulerpartlemgs2  31538  sseqmw  31549  sseqf  31550  sseqp1  31553  fiblem  31556  fibp1  31559  plymul02  31716  signsvtn0  31740  signstres  31745  signshlen  31760  reprinrn  31789  circlemethhgt  31814  txsconnlem  32385  iccllysconn  32395  rellysconn  32396  cvmseu  32421  cvmliftmolem2  32427  cvmliftlem6  32435  cvmliftlem7  32436  cvmliftlem8  32437  cvmliftlem9  32438  cvmliftlem11  32440  cvmliftlem15  32443  cvmlift2lem7  32454  cvmlift2lem10  32457  cvmlift3lem8  32471  cvmlift3lem9  32472  mvrsfpw  32651  mrsubff1  32659  msrid  32690  msrfo  32691  elmsta  32693  mtyf  32697  msubff1  32701  vhmcls  32711  mclsax  32714  elmthm  32721  mthmblem  32725  mclsppslem  32728  iprodefisumlem  32870  soseq  32994  noetalem3  33117  madeval2  33188  fullfunfnv  33305  fullfunfv  33306  tailfb  33623  filnetlem4  33627  taupilem3  34483  icoreresf  34516  icoreelrnab  34518  relowlssretop  34527  relowlpssretop  34528  unccur  34757  matunitlindflem1  34770  matunitlindflem2  34771  ptrecube  34774  poimirlem28  34802  poimirlem32  34806  heicant  34809  opnmbllem0  34810  mblfinlem1  34811  mblfinlem2  34812  volsupnfl  34819  cnambfre  34822  dvtan  34824  itg2addnclem  34825  itg2addnclem2  34826  ftc1anclem3  34851  ftc1anclem5  34853  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  areacirc  34869  indexdom  34892  sdclem2  34900  sstotbnd2  34935  sstotbnd  34936  isbndx  34943  isbnd3b  34946  prdsbnd  34954  prdstotbnd  34955  ismtyhmeolem  34965  heibor1lem  34970  heiborlem1  34972  heibor  34982  rrnequiv  34996  keridl  35193  ellkr  36107  lkr0f  36112  cdleme50rnlem  37562  elrfirn  39172  ismrcd2  39176  isnacs2  39183  nacsfix  39189  mapfzcons1  39194  mzpcompact2lem  39228  eq0rabdioph  39253  eldioph4b  39288  diophren  39290  pw2f1ocnv  39514  pw2f1o2val2  39517  lmhmfgsplit  39566  pwssplit4  39569  hbt  39610  mpaaeu  39630  mendring  39672  proot1mul  39679  proot1hash  39680  proot1ex  39681  deg1mhm  39687  fgraphopab  39690  hausgraph  39692  ofsubid  40536  expgrowthi  40545  expgrowth  40547  binomcxplemdvbinom  40565  binomcxplemcvg  40566  binomcxplemnotnn0  40568  rfcnpre1  41156  rfcnpre2  41168  cncmpmax  41169  rfcnpre3  41170  rfcnpre4  41171  elixpconstg  41235  ffi  41309  dffo3f  41318  islptre  41780  resincncf  42038  dvcosre  42076  dvresntr  42082  volioof  42153  stoweidlem48  42214  fourierdlem12  42285  fourierdlem15  42288  fourierdlem41  42314  fourierdlem42  42315  fourierdlem46  42318  fourierdlem48  42320  fourierdlem49  42321  fourierdlem54  42326  fourierdlem56  42328  fourierdlem62  42334  fourierdlem64  42336  fourierdlem65  42337  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem102  42374  fourierdlem103  42375  fourierdlem104  42376  fourierdlem114  42386  sge0split  42572  elhoi  42705  mbfresmf  42897  fafvelrn  43250  ffnafv  43251  fafv2elrn  43314  fafv2elrnb  43315  imarnf1pr  43362  2ffzoeq  43409  fargshiftfv  43446  fargshiftf  43447  fargshiftf1  43448  fargshiftfo  43449  zrinitorngc  44169  zrtermorngc  44170  zrtermoringc  44239  fdmdifeqresdif  44288  fdivmpt  44498  fdivmptf  44499  refdivmptf  44500  aacllem  44800
  Copyright terms: Public domain W3C validator