Theorem frn 6724

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

Syntax hints:   → wi 4   ⊆ wss 3948  ran crn 5677   Fn wfn 6538  ⟶wf 6539

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 206  df-an 396  df-f 6547

This theorem is referenced by:  frnd  6725  fimass  6738  fimacnv  6739  fco2  6744  fssxp  6745  fimacnvdisj  6769  f00  6773  f0rn0  6776  f1resf1  6796  foconst  6820  ffvelcdm  7083  f1ompt  7112  fnfvrnss  7122  rnmptss  7124  isofr2  7344  fiun  7933  fo1stres  8005  fo2ndres  8006  1stcof  8009  2ndcof  8010  fnwelem  8122  orderseqlem  8148  tposf2  8241  seqomlem2  8457  oacomf1olem  8570  naddunif  8698  naddasslem1  8699  naddasslem2  8700  map0b  8883  mapsnd  8886  fipreima  9364  indexfi  9366  dffi3  9432  oismo  9541  djuin  9919  updjudhcoinlf  9933  updjudhcoinrg  9934  acndom  10052  acndom2  10055  dfac12lem2  10145  dfac12lem3  10146  ackbij1  10239  cfflb  10260  fin23lem40  10352  fin23lem41  10353  isf34lem7  10380  fin1a2lem6  10406  fin1a2lem7  10407  hsmexlem4  10430  hsmexlem5  10431  axdc2lem  10449  axdc3lem2  10452  ttukeylem6  10515  unirnfdomd  10568  pwcfsdom  10584  smobeth  10587  pwfseqlem5  10664  tskurn  10790  wfgru  10817  rpnnen1lem4  12971  rpnnen1lem5  12972  unirnioo  13433  fseqsupcl  13949  fseqsupubi  13950  limsupcl  15424  limsuple  15429  limsupval2  15431  prmreclem6  16861  0ram2  16961  0ramcl  16963  imasdsval2  17469  mrcssv  17565  isacs1i  17608  acsmapd  18517  acsmap2d  18518  gsumval1  18614  dfod2  19480  odcl2  19481  sylow1lem2  19515  efgsfo  19655  gexex  19769  iscyggen2  19797  iscyg3  19802  gsumval3lem1  19821  gsumval3  19823  dprdf1  19951  subgdmdprd  19952  subgdprd  19953  lindfmm  21692  m2cpmmhm  22567  leordtval2  23036  lecldbas  23043  discmp  23222  cmpsub  23224  tgcmp  23225  hauscmplem  23230  2ndcctbss  23279  2ndcsep  23283  comppfsc  23356  kgentop  23366  1stckgen  23378  kgencn2  23381  txuni2  23389  xkoopn  23413  xkouni  23423  xkoccn  23443  ptcnplem  23445  txkgen  23476  xkoco1cn  23481  xkoco2cn  23482  xkococnlem  23483  xkococn  23484  xkoinjcn  23511  hmphdis  23620  zfbas  23720  uzrest  23721  elfm  23771  alexsubALT  23875  efmndtmd  23925  submtmd  23928  symgtgp  23930  tsmsxplem1  23977  blin2  24255  imasf1oxms  24318  tgqioo  24636  xrtgioo  24642  metdscn2  24693  iimulcn  24781  iimulcnOLD  24782  icchmeo  24785  icchmeoOLD  24786  xrhmeo  24791  cnheiborlem  24800  tcphex  25065  tchnmfval  25076  fmcfil  25120  causs  25146  ovolficcss  25318  elovolm  25324  ovoliunlem2  25352  volsup  25405  uniioovol  25428  dyadmbllem  25448  dyadmbl  25449  opnmbllem  25450  opnmblALT  25452  volsup2  25454  mbfconstlem  25476  i1fd  25530  i1f1  25539  itg11  25540  itg1addlem4  25548  itg1addlem4OLD  25549  itg1climres  25564  itg2gt0  25610  limciun  25743  c1liplem1  25849  dvne0f1  25865  dvcnvrelem2  25871  dvcnvre  25872  mdeglt  25921  mdegxrcl  25923  mdegcl  25925  ig1peu  26027  ulmss  26248  reeff1o  26299  efifo  26396  dvlog  26499  efopn  26506  lgamcvg2  26901  dchrisum0fno1  27358  norn  27498  oldf  27698  usgredgss  28853  hhssims  30961  shsss  31000  pjrni  31389  imaelshi  31745  foresf1o  32176  fnpreimac  32330  tocyc01  32714  cycpmrn  32739  cycpmconjslem2  32751  cyc3conja  32753  dimkerim  33167  smatrcl  33241  locfinreflem  33285  esumcvg  33549  omssubadd  33764  sitgclbn  33807  eulerpartgbij  33836  eulerpartlemgvv  33840  eulerpartlemgf  33843  ballotlemsima  33979  hashf1dmcdm  34570  lfuhgr  34573  mrsubf  34973  msubf  34988  mstapst  35003  mclsind  35026  mclsppslem  35039  icoreunrn  36706  pibt2  36764  ptrecube  36954  poimirlem1  36955  poimirlem3  36957  poimirlem12  36966  poimirlem16  36970  poimirlem32  36986  broucube  36988  heicant  36989  opnmbllem0  36990  mblfinlem1  36991  mblfinlem2  36992  mblfinlem3  36993  mblfinlem4  36994  ismblfin  36995  volsupnfl  36999  ftc1anclem5  37031  ftc1anclem7  37033  ftc1anclem8  37034  ftc1anc  37035  indexdom  37068  sstotbnd  37109  prdsbnd  37127  heibor1lem  37143  heiborlem1  37145  rrnval  37161  reheibor  37173  lsatset  38326  elrfirn  41898  isnacs2  41909  nacsfix  41915  coeq0i  41956  diophrw  41962  dnwech  42255  pwssplit4  42296  hbt  42337  rnmptssf  44412  rnmptssff  44440  liminfval2  44945  fourierdlem12  45296  fourierdlem42  45326  fourierdlem54  45337  fourierdlem76  45359  fourierdlem85  45368  fourierdlem88  45371  fourierdlem93  45376  fourierdlem113  45396  hoicvr  45725  vonvolmbl2  45840  vonvol2  45841  fafvelcdm  46339  fafv2elcdm  46403  mgmplusfreseq  47004  elbigolo1  47407  aacllem  48012