Theorem frn 6671

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

Syntax hints:   → wi 4   ⊆ wss 3890  ran crn 5627   Fn wfn 6489  ⟶wf 6490

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 6498

This theorem is referenced by:  frnd  6672  fimass  6684  fimacnv  6686  fco2  6690  fssxp  6691  fimacnvdisj  6714  f00  6718  f0rn0  6721  f1resf1  6740  foconst  6763  ffvelcdm  7029  f1ompt  7059  fnfvrnss  7069  rnmptss  7071  isofr2  7294  fiun  7891  fo1stres  7963  fo2ndres  7964  1stcof  7967  2ndcof  7968  fnwelem  8076  orderseqlem  8102  tposf2  8195  seqomlem2  8385  oacomf1olem  8494  naddunif  8624  naddasslem1  8625  naddasslem2  8626  map0b  8826  mapsnd  8829  fipreima  9263  indexfi  9265  dffi3  9339  oismo  9450  djuin  9837  updjudhcoinlf  9851  updjudhcoinrg  9852  acndom  9968  acndom2  9971  dfac12lem2  10062  dfac12lem3  10063  ackbij1  10154  cfflb  10176  fin23lem40  10268  fin23lem41  10269  isf34lem7  10296  fin1a2lem6  10322  fin1a2lem7  10323  hsmexlem4  10346  hsmexlem5  10347  axdc2lem  10365  axdc3lem2  10368  ttukeylem6  10431  unirnfdomd  10485  pwcfsdom  10501  smobeth  10504  pwfseqlem5  10581  tskurn  10707  wfgru  10734  rpnnen1lem4  12925  rpnnen1lem5  12926  unirnioo  13397  fseqsupcl  13934  fseqsupubi  13935  hashf1dmcdm  14401  limsupcl  15430  limsuple  15435  limsupval2  15437  prmreclem6  16887  0ram2  16987  0ramcl  16989  imasdsval2  17475  mrcssv  17575  isacs1i  17618  acsmapd  18515  acsmap2d  18516  gsumval1  18646  dfod2  19534  odcl2  19535  sylow1lem2  19569  efgsfo  19709  gexex  19823  iscyggen2  19851  iscyg3  19856  gsumval3lem1  19875  gsumval3  19877  dprdf1  20005  subgdmdprd  20006  subgdprd  20007  lindfmm  21821  m2cpmmhm  22724  leordtval2  23191  lecldbas  23198  discmp  23377  cmpsub  23379  tgcmp  23380  hauscmplem  23385  2ndcctbss  23434  2ndcsep  23438  comppfsc  23511  kgentop  23521  1stckgen  23533  kgencn2  23536  txuni2  23544  xkoopn  23568  xkouni  23578  xkoccn  23598  ptcnplem  23600  txkgen  23631  xkoco1cn  23636  xkoco2cn  23637  xkococnlem  23638  xkococn  23639  xkoinjcn  23666  hmphdis  23775  zfbas  23875  uzrest  23876  elfm  23926  alexsubALT  24030  efmndtmd  24080  submtmd  24083  symgtgp  24085  tsmsxplem1  24132  blin2  24408  imasf1oxms  24468  tgqioo  24779  xrtgioo  24786  metdscn2  24837  iimulcn  24919  icchmeo  24922  xrhmeo  24927  cnheiborlem  24935  tcphex  25198  tchnmfval  25209  fmcfil  25253  causs  25279  ovolficcss  25450  elovolm  25456  ovoliunlem2  25484  volsup  25537  uniioovol  25560  dyadmbllem  25580  dyadmbl  25581  opnmbllem  25582  opnmblALT  25584  volsup2  25586  mbfconstlem  25608  i1fd  25662  i1f1  25671  itg11  25672  itg1addlem4  25680  itg1climres  25695  itg2gt0  25741  limciun  25875  c1liplem1  25977  dvne0f1  25993  dvcnvrelem2  25999  dvcnvre  26000  mdeglt  26044  mdegxrcl  26046  mdegcl  26048  ig1peu  26154  ulmss  26379  reeff1o  26429  efifo  26528  dvlog  26632  efopn  26639  lgamcvg2  27036  dchrisum0fno1  27492  norn  27633  oldf  27847  usgredgss  29246  hhssims  31364  shsss  31403  pjrni  31792  imaelshi  32148  foresf1o  32593  fnpreimac  32762  tocyc01  33198  cycpmrn  33223  cycpmconjslem2  33235  cyc3conja  33237  dimkerim  33791  smatrcl  33960  locfinreflem  34004  esumcvg  34250  omssubadd  34464  sitgclbn  34507  eulerpartgbij  34536  eulerpartlemgvv  34540  eulerpartlemgf  34543  ballotlemsima  34680  lfuhgr  35320  mrsubf  35719  msubf  35734  mstapst  35749  mclsind  35772  mclsppslem  35785  icoreunrn  37693  pibt2  37751  ptrecube  37959  poimirlem1  37960  poimirlem3  37962  poimirlem12  37971  poimirlem16  37975  poimirlem32  37991  broucube  37993  heicant  37994  opnmbllem0  37995  mblfinlem1  37996  mblfinlem2  37997  mblfinlem3  37998  mblfinlem4  37999  ismblfin  38000  volsupnfl  38004  ftc1anclem5  38036  ftc1anclem7  38038  ftc1anclem8  38039  ftc1anc  38040  indexdom  38073  sstotbnd  38114  prdsbnd  38132  heibor1lem  38148  heiborlem1  38150  rrnval  38166  reheibor  38178  lsatset  39454  aks6d1c2  42587  aks6d1c6lem3  42629  aks6d1c6isolem1  42631  aks6d1c7lem1  42637  unitscyglem1  42652  elrfirn  43145  isnacs2  43156  nacsfix  43162  coeq0i  43203  diophrw  43209  dnwech  43498  pwssplit4  43539  hbt  43580  rnmptssf  45698  rnmptssff  45725  liminfval2  46218  fourierdlem12  46569  fourierdlem42  46599  fourierdlem54  46610  fourierdlem76  46632  fourierdlem85  46641  fourierdlem88  46644  fourierdlem93  46649  fourierdlem113  46669  hoicvr  46998  vonvolmbl2  47113  vonvol2  47114  fafvelcdm  47634  fafv2elcdm  47698  mgmplusfreseq  48657  elbigolo1  49049  aacllem  50292