Theorem frn 6667

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

Syntax hints:   → wi 4   ⊆ wss 3899  ran crn 5623   Fn wfn 6485  ⟶wf 6486

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 6494

This theorem is referenced by:  frnd  6668  fimass  6680  fimacnv  6682  fco2  6686  fssxp  6687  fimacnvdisj  6710  f00  6714  f0rn0  6717  f1resf1  6736  foconst  6759  ffvelcdm  7024  f1ompt  7054  fnfvrnss  7064  rnmptss  7066  isofr2  7288  fiun  7885  fo1stres  7957  fo2ndres  7958  1stcof  7961  2ndcof  7962  fnwelem  8071  orderseqlem  8097  tposf2  8190  seqomlem2  8380  oacomf1olem  8489  naddunif  8619  naddasslem1  8620  naddasslem2  8621  map0b  8819  mapsnd  8822  fipreima  9256  indexfi  9258  dffi3  9332  oismo  9443  djuin  9828  updjudhcoinlf  9842  updjudhcoinrg  9843  acndom  9959  acndom2  9962  dfac12lem2  10053  dfac12lem3  10054  ackbij1  10145  cfflb  10167  fin23lem40  10259  fin23lem41  10260  isf34lem7  10287  fin1a2lem6  10313  fin1a2lem7  10314  hsmexlem4  10337  hsmexlem5  10338  axdc2lem  10356  axdc3lem2  10359  ttukeylem6  10422  unirnfdomd  10476  pwcfsdom  10492  smobeth  10495  pwfseqlem5  10572  tskurn  10698  wfgru  10725  rpnnen1lem4  12891  rpnnen1lem5  12892  unirnioo  13363  fseqsupcl  13898  fseqsupubi  13899  hashf1dmcdm  14365  limsupcl  15394  limsuple  15399  limsupval2  15401  prmreclem6  16847  0ram2  16947  0ramcl  16949  imasdsval2  17435  mrcssv  17535  isacs1i  17578  acsmapd  18475  acsmap2d  18476  gsumval1  18606  dfod2  19491  odcl2  19492  sylow1lem2  19526  efgsfo  19666  gexex  19780  iscyggen2  19808  iscyg3  19813  gsumval3lem1  19832  gsumval3  19834  dprdf1  19962  subgdmdprd  19963  subgdprd  19964  lindfmm  21780  m2cpmmhm  22687  leordtval2  23154  lecldbas  23161  discmp  23340  cmpsub  23342  tgcmp  23343  hauscmplem  23348  2ndcctbss  23397  2ndcsep  23401  comppfsc  23474  kgentop  23484  1stckgen  23496  kgencn2  23499  txuni2  23507  xkoopn  23531  xkouni  23541  xkoccn  23561  ptcnplem  23563  txkgen  23594  xkoco1cn  23599  xkoco2cn  23600  xkococnlem  23601  xkococn  23602  xkoinjcn  23629  hmphdis  23738  zfbas  23838  uzrest  23839  elfm  23889  alexsubALT  23993  efmndtmd  24043  submtmd  24046  symgtgp  24048  tsmsxplem1  24095  blin2  24371  imasf1oxms  24431  tgqioo  24742  xrtgioo  24749  metdscn2  24800  iimulcn  24888  iimulcnOLD  24889  icchmeo  24892  icchmeoOLD  24893  xrhmeo  24898  cnheiborlem  24907  tcphex  25171  tchnmfval  25182  fmcfil  25226  causs  25252  ovolficcss  25424  elovolm  25430  ovoliunlem2  25458  volsup  25511  uniioovol  25534  dyadmbllem  25554  dyadmbl  25555  opnmbllem  25556  opnmblALT  25558  volsup2  25560  mbfconstlem  25582  i1fd  25636  i1f1  25645  itg11  25646  itg1addlem4  25654  itg1climres  25669  itg2gt0  25715  limciun  25849  c1liplem1  25955  dvne0f1  25971  dvcnvrelem2  25977  dvcnvre  25978  mdeglt  26024  mdegxrcl  26026  mdegcl  26028  ig1peu  26134  ulmss  26360  reeff1o  26411  efifo  26510  dvlog  26614  efopn  26621  lgamcvg2  27019  dchrisum0fno1  27476  norn  27617  oldf  27825  usgredgss  29181  hhssims  31298  shsss  31337  pjrni  31726  imaelshi  32082  foresf1o  32528  fnpreimac  32698  tocyc01  33149  cycpmrn  33174  cycpmconjslem2  33186  cyc3conja  33188  dimkerim  33733  smatrcl  33902  locfinreflem  33946  esumcvg  34192  omssubadd  34406  sitgclbn  34449  eulerpartgbij  34478  eulerpartlemgvv  34482  eulerpartlemgf  34485  ballotlemsima  34622  lfuhgr  35261  mrsubf  35660  msubf  35675  mstapst  35690  mclsind  35713  mclsppslem  35726  icoreunrn  37503  pibt2  37561  ptrecube  37760  poimirlem1  37761  poimirlem3  37763  poimirlem12  37772  poimirlem16  37776  poimirlem32  37792  broucube  37794  heicant  37795  opnmbllem0  37796  mblfinlem1  37797  mblfinlem2  37798  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  volsupnfl  37805  ftc1anclem5  37837  ftc1anclem7  37839  ftc1anclem8  37840  ftc1anc  37841  indexdom  37874  sstotbnd  37915  prdsbnd  37933  heibor1lem  37949  heiborlem1  37951  rrnval  37967  reheibor  37979  lsatset  39189  aks6d1c2  42323  aks6d1c6lem3  42365  aks6d1c6isolem1  42367  aks6d1c7lem1  42373  unitscyglem1  42388  elrfirn  42879  isnacs2  42890  nacsfix  42896  coeq0i  42937  diophrw  42943  dnwech  43232  pwssplit4  43273  hbt  43314  rnmptssf  45433  rnmptssff  45460  liminfval2  45954  fourierdlem12  46305  fourierdlem42  46335  fourierdlem54  46346  fourierdlem76  46368  fourierdlem85  46377  fourierdlem88  46380  fourierdlem93  46385  fourierdlem113  46405  hoicvr  46734  vonvolmbl2  46849  vonvol2  46850  fafvelcdm  47358  fafv2elcdm  47422  mgmplusfreseq  48353  elbigolo1  48745  aacllem  49988