Theorem frn 6698

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 6518	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simprbi 496	1 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3917  ran crn 5642   Fn wfn 6509  ⟶wf 6510

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 6518

This theorem is referenced by:  frnd  6699  fimass  6711  fimacnv  6713  fco2  6717  fssxp  6718  fimacnvdisj  6741  f00  6745  f0rn0  6748  f1resf1  6767  foconst  6790  ffvelcdm  7056  f1ompt  7086  fnfvrnss  7096  rnmptss  7098  isofr2  7322  fiun  7924  fo1stres  7997  fo2ndres  7998  1stcof  8001  2ndcof  8002  fnwelem  8113  orderseqlem  8139  tposf2  8232  seqomlem2  8422  oacomf1olem  8531  naddunif  8660  naddasslem1  8661  naddasslem2  8662  map0b  8859  mapsnd  8862  fipreima  9316  indexfi  9318  dffi3  9389  oismo  9500  djuin  9878  updjudhcoinlf  9892  updjudhcoinrg  9893  acndom  10011  acndom2  10014  dfac12lem2  10105  dfac12lem3  10106  ackbij1  10197  cfflb  10219  fin23lem40  10311  fin23lem41  10312  isf34lem7  10339  fin1a2lem6  10365  fin1a2lem7  10366  hsmexlem4  10389  hsmexlem5  10390  axdc2lem  10408  axdc3lem2  10411  ttukeylem6  10474  unirnfdomd  10527  pwcfsdom  10543  smobeth  10546  pwfseqlem5  10623  tskurn  10749  wfgru  10776  rpnnen1lem4  12946  rpnnen1lem5  12947  unirnioo  13417  fseqsupcl  13949  fseqsupubi  13950  hashf1dmcdm  14416  limsupcl  15446  limsuple  15451  limsupval2  15453  prmreclem6  16899  0ram2  16999  0ramcl  17001  imasdsval2  17486  mrcssv  17582  isacs1i  17625  acsmapd  18520  acsmap2d  18521  gsumval1  18617  dfod2  19501  odcl2  19502  sylow1lem2  19536  efgsfo  19676  gexex  19790  iscyggen2  19818  iscyg3  19823  gsumval3lem1  19842  gsumval3  19844  dprdf1  19972  subgdmdprd  19973  subgdprd  19974  lindfmm  21743  m2cpmmhm  22639  leordtval2  23106  lecldbas  23113  discmp  23292  cmpsub  23294  tgcmp  23295  hauscmplem  23300  2ndcctbss  23349  2ndcsep  23353  comppfsc  23426  kgentop  23436  1stckgen  23448  kgencn2  23451  txuni2  23459  xkoopn  23483  xkouni  23493  xkoccn  23513  ptcnplem  23515  txkgen  23546  xkoco1cn  23551  xkoco2cn  23552  xkococnlem  23553  xkococn  23554  xkoinjcn  23581  hmphdis  23690  zfbas  23790  uzrest  23791  elfm  23841  alexsubALT  23945  efmndtmd  23995  submtmd  23998  symgtgp  24000  tsmsxplem1  24047  blin2  24324  imasf1oxms  24384  tgqioo  24695  xrtgioo  24702  metdscn2  24753  iimulcn  24841  iimulcnOLD  24842  icchmeo  24845  icchmeoOLD  24846  xrhmeo  24851  cnheiborlem  24860  tcphex  25124  tchnmfval  25135  fmcfil  25179  causs  25205  ovolficcss  25377  elovolm  25383  ovoliunlem2  25411  volsup  25464  uniioovol  25487  dyadmbllem  25507  dyadmbl  25508  opnmbllem  25509  opnmblALT  25511  volsup2  25513  mbfconstlem  25535  i1fd  25589  i1f1  25598  itg11  25599  itg1addlem4  25607  itg1climres  25622  itg2gt0  25668  limciun  25802  c1liplem1  25908  dvne0f1  25924  dvcnvrelem2  25930  dvcnvre  25931  mdeglt  25977  mdegxrcl  25979  mdegcl  25981  ig1peu  26087  ulmss  26313  reeff1o  26364  efifo  26463  dvlog  26567  efopn  26574  lgamcvg2  26972  dchrisum0fno1  27429  norn  27570  oldf  27772  usgredgss  29093  hhssims  31210  shsss  31249  pjrni  31638  imaelshi  31994  foresf1o  32440  fnpreimac  32602  tocyc01  33082  cycpmrn  33107  cycpmconjslem2  33119  cyc3conja  33121  dimkerim  33630  smatrcl  33793  locfinreflem  33837  esumcvg  34083  omssubadd  34298  sitgclbn  34341  eulerpartgbij  34370  eulerpartlemgvv  34374  eulerpartlemgf  34377  ballotlemsima  34514  lfuhgr  35112  mrsubf  35511  msubf  35526  mstapst  35541  mclsind  35564  mclsppslem  35577  icoreunrn  37354  pibt2  37412  ptrecube  37621  poimirlem1  37622  poimirlem3  37624  poimirlem12  37633  poimirlem16  37637  poimirlem32  37653  broucube  37655  heicant  37656  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  volsupnfl  37666  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  indexdom  37735  sstotbnd  37776  prdsbnd  37794  heibor1lem  37810  heiborlem1  37812  rrnval  37828  reheibor  37840  lsatset  38990  aks6d1c2  42125  aks6d1c6lem3  42167  aks6d1c6isolem1  42169  aks6d1c7lem1  42175  unitscyglem1  42190  elrfirn  42690  isnacs2  42701  nacsfix  42707  coeq0i  42748  diophrw  42754  dnwech  43044  pwssplit4  43085  hbt  43126  rnmptssf  45248  rnmptssff  45275  liminfval2  45773  fourierdlem12  46124  fourierdlem42  46154  fourierdlem54  46165  fourierdlem76  46187  fourierdlem85  46196  fourierdlem88  46199  fourierdlem93  46204  fourierdlem113  46224  hoicvr  46553  vonvolmbl2  46668  vonvol2  46669  fafvelcdm  47175  fafv2elcdm  47239  mgmplusfreseq  48157  elbigolo1  48550  aacllem  49794