Theorem frn 6675

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

Syntax hints:   → wi 4   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494

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 6502

This theorem is referenced by:  frnd  6676  fimass  6688  fimacnv  6690  fco2  6694  fssxp  6695  fimacnvdisj  6718  f00  6722  f0rn0  6725  f1resf1  6744  foconst  6767  ffvelcdm  7033  f1ompt  7063  fnfvrnss  7073  rnmptss  7075  isofr2  7299  fiun  7896  fo1stres  7968  fo2ndres  7969  1stcof  7972  2ndcof  7973  fnwelem  8081  orderseqlem  8107  tposf2  8200  seqomlem2  8390  oacomf1olem  8499  naddunif  8629  naddasslem1  8630  naddasslem2  8631  map0b  8831  mapsnd  8834  fipreima  9268  indexfi  9270  dffi3  9344  oismo  9455  djuin  9842  updjudhcoinlf  9856  updjudhcoinrg  9857  acndom  9973  acndom2  9976  dfac12lem2  10067  dfac12lem3  10068  ackbij1  10159  cfflb  10181  fin23lem40  10273  fin23lem41  10274  isf34lem7  10301  fin1a2lem6  10327  fin1a2lem7  10328  hsmexlem4  10351  hsmexlem5  10352  axdc2lem  10370  axdc3lem2  10373  ttukeylem6  10436  unirnfdomd  10490  pwcfsdom  10506  smobeth  10509  pwfseqlem5  10586  tskurn  10712  wfgru  10739  rpnnen1lem4  12930  rpnnen1lem5  12931  unirnioo  13402  fseqsupcl  13939  fseqsupubi  13940  hashf1dmcdm  14406  limsupcl  15435  limsuple  15440  limsupval2  15442  prmreclem6  16892  0ram2  16992  0ramcl  16994  imasdsval2  17480  mrcssv  17580  isacs1i  17623  acsmapd  18520  acsmap2d  18521  gsumval1  18651  dfod2  19539  odcl2  19540  sylow1lem2  19574  efgsfo  19714  gexex  19828  iscyggen2  19856  iscyg3  19861  gsumval3lem1  19880  gsumval3  19882  dprdf1  20010  subgdmdprd  20011  subgdprd  20012  lindfmm  21807  m2cpmmhm  22710  leordtval2  23177  lecldbas  23184  discmp  23363  cmpsub  23365  tgcmp  23366  hauscmplem  23371  2ndcctbss  23420  2ndcsep  23424  comppfsc  23497  kgentop  23507  1stckgen  23519  kgencn2  23522  txuni2  23530  xkoopn  23554  xkouni  23564  xkoccn  23584  ptcnplem  23586  txkgen  23617  xkoco1cn  23622  xkoco2cn  23623  xkococnlem  23624  xkococn  23625  xkoinjcn  23652  hmphdis  23761  zfbas  23861  uzrest  23862  elfm  23912  alexsubALT  24016  efmndtmd  24066  submtmd  24069  symgtgp  24071  tsmsxplem1  24118  blin2  24394  imasf1oxms  24454  tgqioo  24765  xrtgioo  24772  metdscn2  24823  iimulcn  24905  icchmeo  24908  xrhmeo  24913  cnheiborlem  24921  tcphex  25184  tchnmfval  25195  fmcfil  25239  causs  25265  ovolficcss  25436  elovolm  25442  ovoliunlem2  25470  volsup  25523  uniioovol  25546  dyadmbllem  25566  dyadmbl  25567  opnmbllem  25568  opnmblALT  25570  volsup2  25572  mbfconstlem  25594  i1fd  25648  i1f1  25657  itg11  25658  itg1addlem4  25666  itg1climres  25681  itg2gt0  25727  limciun  25861  c1liplem1  25963  dvne0f1  25979  dvcnvrelem2  25985  dvcnvre  25986  mdeglt  26030  mdegxrcl  26032  mdegcl  26034  ig1peu  26140  ulmss  26362  reeff1o  26412  efifo  26511  dvlog  26615  efopn  26622  lgamcvg2  27018  dchrisum0fno1  27474  norn  27615  oldf  27829  usgredgss  29228  hhssims  31345  shsss  31384  pjrni  31773  imaelshi  32129  foresf1o  32574  fnpreimac  32743  tocyc01  33179  cycpmrn  33204  cycpmconjslem2  33216  cyc3conja  33218  dimkerim  33771  smatrcl  33940  locfinreflem  33984  esumcvg  34230  omssubadd  34444  sitgclbn  34487  eulerpartgbij  34516  eulerpartlemgvv  34520  eulerpartlemgf  34523  ballotlemsima  34660  lfuhgr  35300  mrsubf  35699  msubf  35714  mstapst  35729  mclsind  35752  mclsppslem  35765  icoreunrn  37675  pibt2  37733  ptrecube  37941  poimirlem1  37942  poimirlem3  37944  poimirlem12  37953  poimirlem16  37957  poimirlem32  37973  broucube  37975  heicant  37976  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  volsupnfl  37986  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  indexdom  38055  sstotbnd  38096  prdsbnd  38114  heibor1lem  38130  heiborlem1  38132  rrnval  38148  reheibor  38160  lsatset  39436  aks6d1c2  42569  aks6d1c6lem3  42611  aks6d1c6isolem1  42613  aks6d1c7lem1  42619  unitscyglem1  42634  elrfirn  43127  isnacs2  43138  nacsfix  43144  coeq0i  43185  diophrw  43191  dnwech  43476  pwssplit4  43517  hbt  43558  rnmptssf  45676  rnmptssff  45703  liminfval2  46196  fourierdlem12  46547  fourierdlem42  46577  fourierdlem54  46588  fourierdlem76  46610  fourierdlem85  46619  fourierdlem88  46622  fourierdlem93  46627  fourierdlem113  46647  hoicvr  46976  vonvolmbl2  47091  vonvol2  47092  fafvelcdm  47618  fafv2elcdm  47682  mgmplusfreseq  48641  elbigolo1  49033  aacllem  50276