Theorem frn 6670

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

Syntax hints:   → wi 4   ⊆ wss 3902  ran crn 5626   Fn wfn 6488  ⟶wf 6489

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 6497

This theorem is referenced by:  frnd  6671  fimass  6683  fimacnv  6685  fco2  6689  fssxp  6690  fimacnvdisj  6713  f00  6717  f0rn0  6720  f1resf1  6739  foconst  6762  ffvelcdm  7028  f1ompt  7058  fnfvrnss  7068  rnmptss  7070  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  9834  updjudhcoinlf  9848  updjudhcoinrg  9849  acndom  9965  acndom2  9968  dfac12lem2  10059  dfac12lem3  10060  ackbij1  10151  cfflb  10173  fin23lem40  10265  fin23lem41  10266  isf34lem7  10293  fin1a2lem6  10319  fin1a2lem7  10320  hsmexlem4  10343  hsmexlem5  10344  axdc2lem  10362  axdc3lem2  10365  ttukeylem6  10428  unirnfdomd  10482  pwcfsdom  10498  smobeth  10501  pwfseqlem5  10578  tskurn  10704  wfgru  10731  rpnnen1lem4  12897  rpnnen1lem5  12898  unirnioo  13369  fseqsupcl  13904  fseqsupubi  13905  hashf1dmcdm  14371  limsupcl  15400  limsuple  15405  limsupval2  15407  prmreclem6  16853  0ram2  16953  0ramcl  16955  imasdsval2  17441  mrcssv  17541  isacs1i  17584  acsmapd  18481  acsmap2d  18482  gsumval1  18612  dfod2  19497  odcl2  19498  sylow1lem2  19532  efgsfo  19672  gexex  19786  iscyggen2  19814  iscyg3  19819  gsumval3lem1  19838  gsumval3  19840  dprdf1  19968  subgdmdprd  19969  subgdprd  19970  lindfmm  21786  m2cpmmhm  22693  leordtval2  23160  lecldbas  23167  discmp  23346  cmpsub  23348  tgcmp  23349  hauscmplem  23354  2ndcctbss  23403  2ndcsep  23407  comppfsc  23480  kgentop  23490  1stckgen  23502  kgencn2  23505  txuni2  23513  xkoopn  23537  xkouni  23547  xkoccn  23567  ptcnplem  23569  txkgen  23600  xkoco1cn  23605  xkoco2cn  23606  xkococnlem  23607  xkococn  23608  xkoinjcn  23635  hmphdis  23744  zfbas  23844  uzrest  23845  elfm  23895  alexsubALT  23999  efmndtmd  24049  submtmd  24052  symgtgp  24054  tsmsxplem1  24101  blin2  24377  imasf1oxms  24437  tgqioo  24748  xrtgioo  24755  metdscn2  24806  iimulcn  24894  iimulcnOLD  24895  icchmeo  24898  icchmeoOLD  24899  xrhmeo  24904  cnheiborlem  24913  tcphex  25177  tchnmfval  25188  fmcfil  25232  causs  25258  ovolficcss  25430  elovolm  25436  ovoliunlem2  25464  volsup  25517  uniioovol  25540  dyadmbllem  25560  dyadmbl  25561  opnmbllem  25562  opnmblALT  25564  volsup2  25566  mbfconstlem  25588  i1fd  25642  i1f1  25651  itg11  25652  itg1addlem4  25660  itg1climres  25675  itg2gt0  25721  limciun  25855  c1liplem1  25961  dvne0f1  25977  dvcnvrelem2  25983  dvcnvre  25984  mdeglt  26030  mdegxrcl  26032  mdegcl  26034  ig1peu  26140  ulmss  26366  reeff1o  26417  efifo  26516  dvlog  26620  efopn  26627  lgamcvg2  27025  dchrisum0fno1  27482  norn  27623  oldf  27837  usgredgss  29236  hhssims  31353  shsss  31392  pjrni  31781  imaelshi  32137  foresf1o  32582  fnpreimac  32751  tocyc01  33202  cycpmrn  33227  cycpmconjslem2  33239  cyc3conja  33241  dimkerim  33786  smatrcl  33955  locfinreflem  33999  esumcvg  34245  omssubadd  34459  sitgclbn  34502  eulerpartgbij  34531  eulerpartlemgvv  34535  eulerpartlemgf  34538  ballotlemsima  34675  lfuhgr  35314  mrsubf  35713  msubf  35728  mstapst  35743  mclsind  35766  mclsppslem  35779  icoreunrn  37566  pibt2  37624  ptrecube  37823  poimirlem1  37824  poimirlem3  37826  poimirlem12  37835  poimirlem16  37839  poimirlem32  37855  broucube  37857  heicant  37858  opnmbllem0  37859  mblfinlem1  37860  mblfinlem2  37861  mblfinlem3  37862  mblfinlem4  37863  ismblfin  37864  volsupnfl  37868  ftc1anclem5  37900  ftc1anclem7  37902  ftc1anclem8  37903  ftc1anc  37904  indexdom  37937  sstotbnd  37978  prdsbnd  37996  heibor1lem  38012  heiborlem1  38014  rrnval  38030  reheibor  38042  lsatset  39318  aks6d1c2  42452  aks6d1c6lem3  42494  aks6d1c6isolem1  42496  aks6d1c7lem1  42502  unitscyglem1  42517  elrfirn  43004  isnacs2  43015  nacsfix  43021  coeq0i  43062  diophrw  43068  dnwech  43357  pwssplit4  43398  hbt  43439  rnmptssf  45558  rnmptssff  45585  liminfval2  46079  fourierdlem12  46430  fourierdlem42  46460  fourierdlem54  46471  fourierdlem76  46493  fourierdlem85  46502  fourierdlem88  46505  fourierdlem93  46510  fourierdlem113  46530  hoicvr  46859  vonvolmbl2  46974  vonvol2  46975  fafvelcdm  47483  fafv2elcdm  47547  mgmplusfreseq  48478  elbigolo1  48870  aacllem  50113