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

Theorem frn 6514
Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frn (𝐹:𝐴𝐵 → ran 𝐹𝐵)

Proof of Theorem frn
StepHypRef Expression
1 df-f 6353 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simprbi 497 1 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
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:  frnd  6515  fco2  6527  fssxp  6528  fimass  6549  fimacnvdisj  6551  f00  6555  f0rn0  6558  f1resf1  6577  foconst  6597  ffvelrn  6842  f1ompt  6868  fnfvrnss  6877  rnmptss  6879  isofr2  7086  fiunw  7632  fiun  7635  fo1stres  7706  fo2ndres  7707  1stcof  7710  2ndcof  7711  fnwelem  7816  tposf2  7907  seqomlem2  8078  oacomf1olem  8180  map0b  8437  mapsnd  8439  fipreima  8819  indexfi  8821  dffi3  8884  oismo  8993  djuin  9336  updjudhcoinlf  9350  updjudhcoinrg  9351  acndom  9466  acndom2  9469  dfac12lem2  9559  dfac12lem3  9560  ackbij1  9649  cfflb  9670  fin23lem40  9762  fin23lem41  9763  isf34lem7  9790  fin1a2lem6  9816  fin1a2lem7  9817  hsmexlem4  9840  hsmexlem5  9841  axdc2lem  9859  axdc3lem2  9862  ttukeylem6  9925  unirnfdomd  9978  pwcfsdom  9994  smobeth  9997  pwfseqlem5  10074  tskurn  10200  wfgru  10227  rpnnen1lem4  12369  rpnnen1lem5  12370  unirnioo  12827  fseqsupcl  13335  fseqsupubi  13336  limsupcl  14820  limsuple  14825  limsupval2  14827  prmreclem6  16247  0ram2  16347  0ramcl  16349  imasdsval2  16779  mrcssv  16875  isacs1i  16918  acsmapd  17778  acsmap2d  17779  gsumval1  17883  dfod2  18622  odcl2  18623  sylow1lem2  18655  efgsfo  18796  gexex  18904  iscyggen2  18931  iscyg3  18936  gsumval3lem1  18956  gsumval3  18958  dprdf1  19086  subgdmdprd  19087  subgdprd  19088  lindfmm  20901  m2cpmmhm  21283  leordtval2  21750  lecldbas  21757  discmp  21936  cmpsub  21938  tgcmp  21939  hauscmplem  21944  2ndcctbss  21993  2ndcsep  21997  comppfsc  22070  kgentop  22080  1stckgen  22092  kgencn2  22095  txuni2  22103  xkoopn  22127  xkouni  22137  xkoccn  22157  ptcnplem  22159  txkgen  22190  xkoco1cn  22195  xkoco2cn  22196  xkococnlem  22197  xkococn  22198  xkoinjcn  22225  hmphdis  22334  zfbas  22434  uzrest  22435  elfm  22485  alexsubALT  22589  symgtgp  22639  submtmd  22642  tsmsxplem1  22690  blin2  22968  imasf1oxms  23028  tgqioo  23337  xrtgioo  23343  metdscn2  23394  iimulcn  23471  icchmeo  23474  xrhmeo  23479  cnheiborlem  23487  tcphex  23749  tchnmfval  23760  fmcfil  23804  causs  23830  ovolficcss  23999  elovolm  24005  ovoliunlem2  24033  volsup  24086  uniioovol  24109  dyadmbllem  24129  dyadmbl  24130  opnmbllem  24131  opnmblALT  24133  volsup2  24135  mbfconstlem  24157  i1fd  24211  i1f1  24220  itg11  24221  itg1addlem4  24229  itg1climres  24244  itg2gt0  24290  limciun  24421  c1liplem1  24522  dvne0f1  24538  dvcnvrelem2  24544  dvcnvre  24545  mdeglt  24588  mdegxrcl  24590  mdegcl  24592  ig1peu  24694  ulmss  24914  reeff1o  24964  efifo  25058  dvlog  25161  efopn  25168  lgamcvg2  25560  dchrisum0fno1  26015  usgredgss  26872  hhssims  28979  shsss  29018  pjrni  29407  imaelshi  29763  foresf1o  30193  fnpreimac  30345  tocyc01  30688  cycpmrn  30713  cycpmconjslem2  30725  cyc3conja  30727  dimkerim  30923  smatrcl  30961  locfinreflem  31004  esumcvg  31245  omssubadd  31458  sitgclbn  31501  eulerpartgbij  31530  eulerpartlemgvv  31534  eulerpartlemgf  31537  ballotlemsima  31673  hashf1dmcdm  32254  lfuhgr  32262  mrsubf  32662  msubf  32677  mstapst  32692  mclsind  32715  mclsppslem  32728  orderseqlem  32992  norn  33056  icoreunrn  34523  pibt2  34581  ptrecube  34774  poimirlem1  34775  poimirlem3  34777  poimirlem12  34786  poimirlem16  34790  poimirlem32  34806  broucube  34808  heicant  34809  opnmbllem0  34810  mblfinlem1  34811  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  volsupnfl  34819  ftc1anclem5  34853  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  indexdom  34892  sstotbnd  34936  prdsbnd  34954  heibor1lem  34970  heiborlem1  34972  rrnval  34988  reheibor  35000  lsatset  36008  elrfirn  39172  isnacs2  39183  nacsfix  39189  coeq0i  39230  diophrw  39236  dnwech  39528  pwssplit4  39569  hbt  39610  rnmptssf  41399  liminfval2  41929  fourierdlem12  42285  fourierdlem42  42315  fourierdlem54  42326  fourierdlem76  42348  fourierdlem85  42357  fourierdlem88  42360  fourierdlem93  42365  fourierdlem113  42385  hoicvr  42711  vonvolmbl2  42826  vonvol2  42827  fafvelrn  43250  fafv2elrn  43314  mgmplusfreseq  43887  efmndtmd  43967  elbigolo1  44515  aacllem  44800
  Copyright terms: Public domain W3C validator