Theorem frn 6695

Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
frn	⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

Proof of Theorem frn

Step	Hyp	Ref	Expression
1		df-f 6515	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simprbi 496	1 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3914  ran crn 5639   Fn wfn 6506  ⟶wf 6507

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 207  df-an 396  df-f 6515

This theorem is referenced by:  frnd  6696  fimass  6708  fimacnv  6710  fco2  6714  fssxp  6715  fimacnvdisj  6738  f00  6742  f0rn0  6745  f1resf1  6764  foconst  6787  ffvelcdm  7053  f1ompt  7083  fnfvrnss  7093  rnmptss  7095  isofr2  7319  fiun  7921  fo1stres  7994  fo2ndres  7995  1stcof  7998  2ndcof  7999  fnwelem  8110  orderseqlem  8136  tposf2  8229  seqomlem2  8419  oacomf1olem  8528  naddunif  8657  naddasslem1  8658  naddasslem2  8659  map0b  8856  mapsnd  8859  fipreima  9309  indexfi  9311  dffi3  9382  oismo  9493  djuin  9871  updjudhcoinlf  9885  updjudhcoinrg  9886  acndom  10004  acndom2  10007  dfac12lem2  10098  dfac12lem3  10099  ackbij1  10190  cfflb  10212  fin23lem40  10304  fin23lem41  10305  isf34lem7  10332  fin1a2lem6  10358  fin1a2lem7  10359  hsmexlem4  10382  hsmexlem5  10383  axdc2lem  10401  axdc3lem2  10404  ttukeylem6  10467  unirnfdomd  10520  pwcfsdom  10536  smobeth  10539  pwfseqlem5  10616  tskurn  10742  wfgru  10769  rpnnen1lem4  12939  rpnnen1lem5  12940  unirnioo  13410  fseqsupcl  13942  fseqsupubi  13943  hashf1dmcdm  14409  limsupcl  15439  limsuple  15444  limsupval2  15446  prmreclem6  16892  0ram2  16992  0ramcl  16994  imasdsval2  17479  mrcssv  17575  isacs1i  17618  acsmapd  18513  acsmap2d  18514  gsumval1  18610  dfod2  19494  odcl2  19495  sylow1lem2  19529  efgsfo  19669  gexex  19783  iscyggen2  19811  iscyg3  19816  gsumval3lem1  19835  gsumval3  19837  dprdf1  19965  subgdmdprd  19966  subgdprd  19967  lindfmm  21736  m2cpmmhm  22632  leordtval2  23099  lecldbas  23106  discmp  23285  cmpsub  23287  tgcmp  23288  hauscmplem  23293  2ndcctbss  23342  2ndcsep  23346  comppfsc  23419  kgentop  23429  1stckgen  23441  kgencn2  23444  txuni2  23452  xkoopn  23476  xkouni  23486  xkoccn  23506  ptcnplem  23508  txkgen  23539  xkoco1cn  23544  xkoco2cn  23545  xkococnlem  23546  xkococn  23547  xkoinjcn  23574  hmphdis  23683  zfbas  23783  uzrest  23784  elfm  23834  alexsubALT  23938  efmndtmd  23988  submtmd  23991  symgtgp  23993  tsmsxplem1  24040  blin2  24317  imasf1oxms  24377  tgqioo  24688  xrtgioo  24695  metdscn2  24746  iimulcn  24834  iimulcnOLD  24835  icchmeo  24838  icchmeoOLD  24839  xrhmeo  24844  cnheiborlem  24853  tcphex  25117  tchnmfval  25128  fmcfil  25172  causs  25198  ovolficcss  25370  elovolm  25376  ovoliunlem2  25404  volsup  25457  uniioovol  25480  dyadmbllem  25500  dyadmbl  25501  opnmbllem  25502  opnmblALT  25504  volsup2  25506  mbfconstlem  25528  i1fd  25582  i1f1  25591  itg11  25592  itg1addlem4  25600  itg1climres  25615  itg2gt0  25661  limciun  25795  c1liplem1  25901  dvne0f1  25917  dvcnvrelem2  25923  dvcnvre  25924  mdeglt  25970  mdegxrcl  25972  mdegcl  25974  ig1peu  26080  ulmss  26306  reeff1o  26357  efifo  26456  dvlog  26560  efopn  26567  lgamcvg2  26965  dchrisum0fno1  27422  norn  27563  oldf  27765  usgredgss  29086  hhssims  31203  shsss  31242  pjrni  31631  imaelshi  31987  foresf1o  32433  fnpreimac  32595  tocyc01  33075  cycpmrn  33100  cycpmconjslem2  33112  cyc3conja  33114  dimkerim  33623  smatrcl  33786  locfinreflem  33830  esumcvg  34076  omssubadd  34291  sitgclbn  34334  eulerpartgbij  34363  eulerpartlemgvv  34367  eulerpartlemgf  34370  ballotlemsima  34507  lfuhgr  35105  mrsubf  35504  msubf  35519  mstapst  35534  mclsind  35557  mclsppslem  35570  icoreunrn  37347  pibt2  37405  ptrecube  37614  poimirlem1  37615  poimirlem3  37617  poimirlem12  37626  poimirlem16  37630  poimirlem32  37646  broucube  37648  heicant  37649  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  volsupnfl  37659  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  indexdom  37728  sstotbnd  37769  prdsbnd  37787  heibor1lem  37803  heiborlem1  37805  rrnval  37821  reheibor  37833  lsatset  38983  aks6d1c2  42118  aks6d1c6lem3  42160  aks6d1c6isolem1  42162  aks6d1c7lem1  42168  unitscyglem1  42183  elrfirn  42683  isnacs2  42694  nacsfix  42700  coeq0i  42741  diophrw  42747  dnwech  43037  pwssplit4  43078  hbt  43119  rnmptssf  45241  rnmptssff  45268  liminfval2  45766  fourierdlem12  46117  fourierdlem42  46147  fourierdlem54  46158  fourierdlem76  46180  fourierdlem85  46189  fourierdlem88  46192  fourierdlem93  46197  fourierdlem113  46217  hoicvr  46546  vonvolmbl2  46661  vonvol2  46662  fafvelcdm  47171  fafv2elcdm  47235  mgmplusfreseq  48153  elbigolo1  48546  aacllem  49790