Theorem frn 6666

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

Syntax hints:   → wi 4   ⊆ wss 3885  ran crn 5622   Fn wfn 6484  ⟶wf 6485

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 209  df-an 398  df-f 6493

This theorem is referenced by:  frnd  6667  fimass  6679  fimacnv  6681  fco2  6685  fssxp  6686  fimacnvdisj  6709  f00  6713  f0rn0  6716  f1resf1  6735  foconst  6758  ffvelcdm  7026  f1ompt  7056  fnfvrnss  7066  rnmptss  7068  isofr2  7292  fiun  7889  fo1stres  7961  fo2ndres  7962  1stcof  7965  2ndcof  7966  fnwelem  8075  orderseqlem  8101  tposf2  8194  seqomlem2  8384  oacomf1olem  8493  naddunif  8623  naddasslem1  8624  naddasslem2  8625  map0b  8825  mapsnd  8828  fipreima  9262  indexfi  9264  dffi3  9338  oismo  9449  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  21806  m2cpmmhm  22732  leordtval2  23199  lecldbas  23206  discmp  23385  cmpsub  23387  tgcmp  23388  hauscmplem  23393  2ndcctbss  23442  2ndcsep  23446  comppfsc  23519  kgentop  23529  1stckgen  23541  kgencn2  23544  txuni2  23552  xkoopn  23576  xkouni  23586  xkoccn  23606  ptcnplem  23608  txkgen  23639  xkoco1cn  23644  xkoco2cn  23645  xkococnlem  23646  xkococn  23647  xkoinjcn  23674  hmphdis  23783  zfbas  23883  uzrest  23884  elfm  23934  alexsubALT  24038  efmndtmd  24088  submtmd  24091  symgtgp  24093  tsmsxplem1  24140  blin2  24416  imasf1oxms  24476  tgqioo  24787  xrtgioo  24794  metdscn2  24845  iimulcn  24927  icchmeo  24930  xrhmeo  24935  cnheiborlem  24943  tcphex  25206  tchnmfval  25217  fmcfil  25261  causs  25287  ovolficcss  25458  elovolm  25464  ovoliunlem2  25492  volsup  25545  uniioovol  25568  dyadmbllem  25588  dyadmbl  25589  opnmbllem  25590  opnmblALT  25592  volsup2  25594  mbfconstlem  25616  i1fd  25670  i1f1  25679  itg11  25680  itg1addlem4  25688  itg1climres  25703  itg2gt0  25749  limciun  25883  c1liplem1  25985  dvne0f1  26001  dvcnvrelem2  26007  dvcnvre  26008  mdeglt  26052  mdegxrcl  26054  mdegcl  26056  ig1peu  26162  ulmss  26384  reeff1o  26434  efifo  26533  dvlog  26637  efopn  26644  lgamcvg2  27040  dchrisum0fno1  27496  norn  27637  oldf  27851  usgredgss  29250  hhssims  31367  shsss  31406  pjrni  31795  imaelshi  32151  foresf1o  32596  fnpreimac  32766  tocyc01  33203  cycpmrn  33228  cycpmconjslem2  33240  cyc3conja  33242  dimkerim  33823  smatrcl  33992  locfinreflem  34036  esumcvg  34282  omssubadd  34496  sitgclbn  34539  eulerpartgbij  34568  eulerpartlemgvv  34572  eulerpartlemgf  34575  ballotlemsima  34712  lfuhgr  35361  mrsubf  35760  msubf  35775  mstapst  35790  mclsind  35813  mclsppslem  35826  icoreunrn  37736  pibt2  37794  ptrecube  38002  poimirlem1  38003  poimirlem3  38005  poimirlem12  38014  poimirlem16  38018  poimirlem32  38034  broucube  38036  heicant  38037  opnmbllem0  38038  mblfinlem1  38039  mblfinlem2  38040  mblfinlem3  38041  mblfinlem4  38042  ismblfin  38043  volsupnfl  38047  ftc1anclem5  38079  ftc1anclem7  38081  ftc1anclem8  38082  ftc1anc  38083  indexdom  38116  sstotbnd  38157  prdsbnd  38175  heibor1lem  38191  heiborlem1  38193  rrnval  38209  reheibor  38221  lsatset  39497  aks6d1c2  42630  aks6d1c6lem3  42672  aks6d1c6isolem1  42674  aks6d1c7lem1  42680  unitscyglem1  42695  elrfirn  43159  isnacs2  43170  nacsfix  43176  coeq0i  43217  diophrw  43223  dnwech  43508  pwssplit4  43549  hbt  43590  rnmptssf  45705  rnmptssff  45732  liminfval2  46225  fourierdlem12  46576  fourierdlem42  46606  fourierdlem54  46617  fourierdlem76  46639  fourierdlem85  46648  fourierdlem88  46651  fourierdlem93  46656  fourierdlem113  46676  hoicvr  47005  vonvolmbl2  47120  vonvol2  47121  fafvelcdm  47647  fafv2elcdm  47711  mgmplusfreseq  48670  elbigolo1  49062  aacllem  50305