Theorem frn 6716

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

Syntax hints:   → wi 4   ⊆ wss 3913  ran crn 5665   Fn wfn 6534  ⟶wf 6535

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 210  df-an 401  df-f 6543

This theorem is referenced by:  frnd  6717  fimass  6729  fimacnv  6731  fco2  6735  fssxp  6736  fimacnvdisj  6759  f00  6763  f0rn0  6766  f1resf1  6787  foconst  6810  ffvelcdm  7079  f1ompt  7109  fnfvrnss  7119  rnmptss  7121  isofr2  7345  fiun  7942  fo1stres  8014  fo2ndres  8015  1stcof  8018  2ndcof  8019  fnwelem  8129  orderseqlem  8155  tposf2  8248  seqomlem2  8440  oacomf1olem  8551  naddunif  8682  naddasslem1  8683  naddasslem2  8684  map0b  8883  mapsnd  8886  fipreima  9317  indexfi  9319  dffi3  9393  oismo  9504  djuin  9906  updjudhcoinlf  9920  updjudhcoinrg  9921  acndom  10037  acndom2  10040  dfac12lem2  10130  dfac12lem3  10131  ackbij1  10222  cfflb  10245  fin23lem40  10337  fin23lem41  10338  isf34lem7  10365  fin1a2lem6  10391  fin1a2lem7  10392  hsmexlem4  10415  hsmexlem5  10416  axdc2lem  10434  axdc3lem2  10437  ttukeylem6  10500  unirnfdomd  10554  pwcfsdom  10570  smobeth  10573  pwfseqlem5  10650  tskurn  10776  wfgru  10803  rpnnen1lem4  13006  rpnnen1lem5  13007  unirnioo  13478  fseqsupcl  14015  fseqsupubi  14016  hashf1dmcdm  14483  limsupcl  15526  limsuple  15531  limsupval2  15533  prmreclem6  16983  0ram2  17083  0ramcl  17085  imasdsval2  17572  mrcssv  17672  isacs1i  17715  acsmapd  18612  acsmap2d  18613  gsumval1  18743  dfod2  19636  odcl2  19637  sylow1lem2  19671  efgsfo  19811  gexex  19925  iscyggen2  19953  iscyg3  19958  gsumval3lem1  19977  gsumval3  19979  dprdf1  20107  subgdmdprd  20108  subgdprd  20109  lindfmm  21948  m2cpmmhm  22873  leordtval2  23340  lecldbas  23347  discmp  23526  cmpsub  23528  tgcmp  23529  hauscmplem  23534  2ndcctbss  23583  2ndcsep  23587  comppfsc  23660  kgentop  23670  1stckgen  23682  kgencn2  23685  txuni2  23693  xkoopn  23717  xkouni  23727  xkoccn  23747  ptcnplem  23749  txkgen  23780  xkoco1cn  23785  xkoco2cn  23786  xkococnlem  23787  xkococn  23788  xkoinjcn  23815  hmphdis  23924  zfbas  24024  uzrest  24025  elfm  24075  alexsubALT  24179  efmndtmd  24229  submtmd  24232  symgtgp  24234  tsmsxplem1  24281  blin2  24557  imasf1oxms  24617  tgqioo  24928  xrtgioo  24935  metdscn2  24986  iimulcn  25068  icchmeo  25071  xrhmeo  25076  cnheiborlem  25084  tcphex  25347  tchnmfval  25358  fmcfil  25402  causs  25428  ovolficcss  25599  elovolm  25605  ovoliunlem2  25633  volsup  25686  uniioovol  25709  dyadmbllem  25729  dyadmbl  25730  opnmbllem  25731  opnmblALT  25733  volsup2  25735  mbfconstlem  25757  i1fd  25811  i1f1  25820  itg11  25821  itg1addlem4  25829  itg1climres  25844  itg2gt0  25890  limciun  26024  c1liplem1  26126  dvne0f1  26142  dvcnvrelem2  26148  dvcnvre  26149  mdeglt  26193  mdegxrcl  26195  mdegcl  26197  ig1peu  26303  ulmss  26528  reeff1o  26578  efifo  26680  dvlog  26784  efopn  26791  lgamcvg2  27187  dchrisum0fno1  27643  norn  27783  oldf  27998  usgredgss  29452  hhssims  31569  shsss  31608  pjrni  31997  imaelshi  32353  foresf1o  32793  fnpreimac  32958  tocyc01  33381  cycpmrn  33406  cycpmconjslem2  33418  cyc3conja  33420  dimkerim  33964  smatrcl  34133  locfinreflem  34177  esumcvg  34423  omssubadd  34637  sitgclbn  34680  eulerpartgbij  34709  eulerpartlemgvv  34713  eulerpartlemgf  34716  ballotlemsima  34853  lfuhgr  35545  mrsubf  35944  msubf  35959  mstapst  35974  mclsind  35997  mclsppslem  36010  icoreunrn  37930  pibt2  37988  ptrecube  38196  poimirlem1  38197  poimirlem3  38199  poimirlem12  38208  poimirlem16  38212  poimirlem32  38228  broucube  38230  heicant  38231  opnmbllem0  38232  mblfinlem1  38233  mblfinlem2  38234  mblfinlem3  38235  mblfinlem4  38236  ismblfin  38237  volsupnfl  38241  ftc1anclem5  38273  ftc1anclem7  38275  ftc1anclem8  38276  ftc1anc  38277  indexdom  38310  sstotbnd  38351  prdsbnd  38369  heibor1lem  38385  heiborlem1  38387  rrnval  38403  reheibor  38415  lsatset  39691  aks6d1c2  42824  aks6d1c6lem3  42866  aks6d1c6isolem1  42868  aks6d1c7lem1  42874  unitscyglem1  42889  elrfirn  43355  isnacs2  43366  nacsfix  43372  coeq0i  43413  diophrw  43419  dnwech  43704  pwssplit4  43745  hbt  43786  rnmptssf  45891  rnmptssff  45918  liminfval2  46411  fourierdlem12  46762  fourierdlem42  46792  fourierdlem54  46803  fourierdlem76  46825  fourierdlem85  46834  fourierdlem88  46837  fourierdlem93  46842  hoicvr  47191  vonvolmbl2  47306  vonvol2  47307  fafvelcdm  47833  fafv2elcdm  47897  mgmplusfreseq  48856  elbigolo1  49259  aacllem  50512