Theorem frn 6658

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

Syntax hints:   → wi 4   ⊆ wss 3897  ran crn 5615   Fn wfn 6476  ⟶wf 6477

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 6485

This theorem is referenced by:  frnd  6659  fimass  6671  fimacnv  6673  fco2  6677  fssxp  6678  fimacnvdisj  6701  f00  6705  f0rn0  6708  f1resf1  6727  foconst  6750  ffvelcdm  7014  f1ompt  7044  fnfvrnss  7054  rnmptss  7056  isofr2  7278  fiun  7875  fo1stres  7947  fo2ndres  7948  1stcof  7951  2ndcof  7952  fnwelem  8061  orderseqlem  8087  tposf2  8180  seqomlem2  8370  oacomf1olem  8479  naddunif  8608  naddasslem1  8609  naddasslem2  8610  map0b  8807  mapsnd  8810  fipreima  9242  indexfi  9244  dffi3  9315  oismo  9426  djuin  9811  updjudhcoinlf  9825  updjudhcoinrg  9826  acndom  9942  acndom2  9945  dfac12lem2  10036  dfac12lem3  10037  ackbij1  10128  cfflb  10150  fin23lem40  10242  fin23lem41  10243  isf34lem7  10270  fin1a2lem6  10296  fin1a2lem7  10297  hsmexlem4  10320  hsmexlem5  10321  axdc2lem  10339  axdc3lem2  10342  ttukeylem6  10405  unirnfdomd  10458  pwcfsdom  10474  smobeth  10477  pwfseqlem5  10554  tskurn  10680  wfgru  10707  rpnnen1lem4  12878  rpnnen1lem5  12879  unirnioo  13349  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  18591  dfod2  19476  odcl2  19477  sylow1lem2  19511  efgsfo  19651  gexex  19765  iscyggen2  19793  iscyg3  19798  gsumval3lem1  19817  gsumval3  19819  dprdf1  19947  subgdmdprd  19948  subgdprd  19949  lindfmm  21764  m2cpmmhm  22660  leordtval2  23127  lecldbas  23134  discmp  23313  cmpsub  23315  tgcmp  23316  hauscmplem  23321  2ndcctbss  23370  2ndcsep  23374  comppfsc  23447  kgentop  23457  1stckgen  23469  kgencn2  23472  txuni2  23480  xkoopn  23504  xkouni  23514  xkoccn  23534  ptcnplem  23536  txkgen  23567  xkoco1cn  23572  xkoco2cn  23573  xkococnlem  23574  xkococn  23575  xkoinjcn  23602  hmphdis  23711  zfbas  23811  uzrest  23812  elfm  23862  alexsubALT  23966  efmndtmd  24016  submtmd  24019  symgtgp  24021  tsmsxplem1  24068  blin2  24344  imasf1oxms  24404  tgqioo  24715  xrtgioo  24722  metdscn2  24773  iimulcn  24861  iimulcnOLD  24862  icchmeo  24865  icchmeoOLD  24866  xrhmeo  24871  cnheiborlem  24880  tcphex  25144  tchnmfval  25155  fmcfil  25199  causs  25225  ovolficcss  25397  elovolm  25403  ovoliunlem2  25431  volsup  25484  uniioovol  25507  dyadmbllem  25527  dyadmbl  25528  opnmbllem  25529  opnmblALT  25531  volsup2  25533  mbfconstlem  25555  i1fd  25609  i1f1  25618  itg11  25619  itg1addlem4  25627  itg1climres  25642  itg2gt0  25688  limciun  25822  c1liplem1  25928  dvne0f1  25944  dvcnvrelem2  25950  dvcnvre  25951  mdeglt  25997  mdegxrcl  25999  mdegcl  26001  ig1peu  26107  ulmss  26333  reeff1o  26384  efifo  26483  dvlog  26587  efopn  26594  lgamcvg2  26992  dchrisum0fno1  27449  norn  27590  oldf  27798  usgredgss  29137  hhssims  31254  shsss  31293  pjrni  31682  imaelshi  32038  foresf1o  32484  fnpreimac  32653  tocyc01  33087  cycpmrn  33112  cycpmconjslem2  33124  cyc3conja  33126  dimkerim  33640  smatrcl  33809  locfinreflem  33853  esumcvg  34099  omssubadd  34313  sitgclbn  34356  eulerpartgbij  34385  eulerpartlemgvv  34389  eulerpartlemgf  34392  ballotlemsima  34529  lfuhgr  35162  mrsubf  35561  msubf  35576  mstapst  35591  mclsind  35614  mclsppslem  35627  icoreunrn  37403  pibt2  37461  ptrecube  37659  poimirlem1  37660  poimirlem3  37662  poimirlem12  37671  poimirlem16  37675  poimirlem32  37691  broucube  37693  heicant  37694  opnmbllem0  37695  mblfinlem1  37696  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  volsupnfl  37704  ftc1anclem5  37736  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  indexdom  37773  sstotbnd  37814  prdsbnd  37832  heibor1lem  37848  heiborlem1  37850  rrnval  37866  reheibor  37878  lsatset  39088  aks6d1c2  42222  aks6d1c6lem3  42264  aks6d1c6isolem1  42266  aks6d1c7lem1  42272  unitscyglem1  42287  elrfirn  42787  isnacs2  42798  nacsfix  42804  coeq0i  42845  diophrw  42851  dnwech  43140  pwssplit4  43181  hbt  43222  rnmptssf  45343  rnmptssff  45370  liminfval2  45865  fourierdlem12  46216  fourierdlem42  46246  fourierdlem54  46257  fourierdlem76  46279  fourierdlem85  46288  fourierdlem88  46291  fourierdlem93  46296  fourierdlem113  46316  hoicvr  46645  vonvolmbl2  46760  vonvol2  46761  fafvelcdm  47269  fafv2elcdm  47333  mgmplusfreseq  48264  elbigolo1  48657  aacllem  49901