Theorem frn 6659

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

Syntax hints:   → wi 4   ⊆ wss 3903  ran crn 5620   Fn wfn 6477  ⟶wf 6478

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 6486

This theorem is referenced by:  frnd  6660  fimass  6672  fimacnv  6674  fco2  6678  fssxp  6679  fimacnvdisj  6702  f00  6706  f0rn0  6709  f1resf1  6728  foconst  6751  ffvelcdm  7015  f1ompt  7045  fnfvrnss  7055  rnmptss  7057  isofr2  7281  fiun  7878  fo1stres  7950  fo2ndres  7951  1stcof  7954  2ndcof  7955  fnwelem  8064  orderseqlem  8090  tposf2  8183  seqomlem2  8373  oacomf1olem  8482  naddunif  8611  naddasslem1  8612  naddasslem2  8613  map0b  8810  mapsnd  8813  fipreima  9248  indexfi  9250  dffi3  9321  oismo  9432  djuin  9814  updjudhcoinlf  9828  updjudhcoinrg  9829  acndom  9945  acndom2  9948  dfac12lem2  10039  dfac12lem3  10040  ackbij1  10131  cfflb  10153  fin23lem40  10245  fin23lem41  10246  isf34lem7  10273  fin1a2lem6  10299  fin1a2lem7  10300  hsmexlem4  10323  hsmexlem5  10324  axdc2lem  10342  axdc3lem2  10345  ttukeylem6  10408  unirnfdomd  10461  pwcfsdom  10477  smobeth  10480  pwfseqlem5  10557  tskurn  10683  wfgru  10710  rpnnen1lem4  12881  rpnnen1lem5  12882  unirnioo  13352  fseqsupcl  13884  fseqsupubi  13885  hashf1dmcdm  14351  limsupcl  15380  limsuple  15385  limsupval2  15387  prmreclem6  16833  0ram2  16933  0ramcl  16935  imasdsval2  17420  mrcssv  17520  isacs1i  17563  acsmapd  18460  acsmap2d  18461  gsumval1  18557  dfod2  19443  odcl2  19444  sylow1lem2  19478  efgsfo  19618  gexex  19732  iscyggen2  19760  iscyg3  19765  gsumval3lem1  19784  gsumval3  19786  dprdf1  19914  subgdmdprd  19915  subgdprd  19916  lindfmm  21734  m2cpmmhm  22630  leordtval2  23097  lecldbas  23104  discmp  23283  cmpsub  23285  tgcmp  23286  hauscmplem  23291  2ndcctbss  23340  2ndcsep  23344  comppfsc  23417  kgentop  23427  1stckgen  23439  kgencn2  23442  txuni2  23450  xkoopn  23474  xkouni  23484  xkoccn  23504  ptcnplem  23506  txkgen  23537  xkoco1cn  23542  xkoco2cn  23543  xkococnlem  23544  xkococn  23545  xkoinjcn  23572  hmphdis  23681  zfbas  23781  uzrest  23782  elfm  23832  alexsubALT  23936  efmndtmd  23986  submtmd  23989  symgtgp  23991  tsmsxplem1  24038  blin2  24315  imasf1oxms  24375  tgqioo  24686  xrtgioo  24693  metdscn2  24744  iimulcn  24832  iimulcnOLD  24833  icchmeo  24836  icchmeoOLD  24837  xrhmeo  24842  cnheiborlem  24851  tcphex  25115  tchnmfval  25126  fmcfil  25170  causs  25196  ovolficcss  25368  elovolm  25374  ovoliunlem2  25402  volsup  25455  uniioovol  25478  dyadmbllem  25498  dyadmbl  25499  opnmbllem  25500  opnmblALT  25502  volsup2  25504  mbfconstlem  25526  i1fd  25580  i1f1  25589  itg11  25590  itg1addlem4  25598  itg1climres  25613  itg2gt0  25659  limciun  25793  c1liplem1  25899  dvne0f1  25915  dvcnvrelem2  25921  dvcnvre  25922  mdeglt  25968  mdegxrcl  25970  mdegcl  25972  ig1peu  26078  ulmss  26304  reeff1o  26355  efifo  26454  dvlog  26558  efopn  26565  lgamcvg2  26963  dchrisum0fno1  27420  norn  27561  oldf  27767  usgredgss  29104  hhssims  31218  shsss  31257  pjrni  31646  imaelshi  32002  foresf1o  32448  fnpreimac  32615  tocyc01  33061  cycpmrn  33086  cycpmconjslem2  33098  cyc3conja  33100  dimkerim  33600  smatrcl  33769  locfinreflem  33813  esumcvg  34059  omssubadd  34274  sitgclbn  34317  eulerpartgbij  34346  eulerpartlemgvv  34350  eulerpartlemgf  34353  ballotlemsima  34490  lfuhgr  35101  mrsubf  35500  msubf  35515  mstapst  35530  mclsind  35553  mclsppslem  35566  icoreunrn  37343  pibt2  37401  ptrecube  37610  poimirlem1  37611  poimirlem3  37613  poimirlem12  37622  poimirlem16  37626  poimirlem32  37642  broucube  37644  heicant  37645  opnmbllem0  37646  mblfinlem1  37647  mblfinlem2  37648  mblfinlem3  37649  mblfinlem4  37650  ismblfin  37651  volsupnfl  37655  ftc1anclem5  37687  ftc1anclem7  37689  ftc1anclem8  37690  ftc1anc  37691  indexdom  37724  sstotbnd  37765  prdsbnd  37783  heibor1lem  37799  heiborlem1  37801  rrnval  37817  reheibor  37829  lsatset  38979  aks6d1c2  42113  aks6d1c6lem3  42155  aks6d1c6isolem1  42157  aks6d1c7lem1  42163  unitscyglem1  42178  elrfirn  42678  isnacs2  42689  nacsfix  42695  coeq0i  42736  diophrw  42742  dnwech  43031  pwssplit4  43072  hbt  43113  rnmptssf  45235  rnmptssff  45262  liminfval2  45759  fourierdlem12  46110  fourierdlem42  46140  fourierdlem54  46151  fourierdlem76  46173  fourierdlem85  46182  fourierdlem88  46185  fourierdlem93  46190  fourierdlem113  46210  hoicvr  46539  vonvolmbl2  46654  vonvol2  46655  fafvelcdm  47164  fafv2elcdm  47228  mgmplusfreseq  48159  elbigolo1  48552  aacllem  49796