Theorem frn 6743

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

Syntax hints:   → wi 4   ⊆ wss 3951  ran crn 5686   Fn wfn 6556  ⟶wf 6557

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 6565

This theorem is referenced by:  frnd  6744  fimass  6756  fimacnv  6758  fco2  6762  fssxp  6763  fimacnvdisj  6786  f00  6790  f0rn0  6793  f1resf1  6812  foconst  6835  ffvelcdm  7101  f1ompt  7131  fnfvrnss  7141  rnmptss  7143  isofr2  7364  fiun  7967  fo1stres  8040  fo2ndres  8041  1stcof  8044  2ndcof  8045  fnwelem  8156  orderseqlem  8182  tposf2  8275  seqomlem2  8491  oacomf1olem  8602  naddunif  8731  naddasslem1  8732  naddasslem2  8733  map0b  8923  mapsnd  8926  fipreima  9398  indexfi  9400  dffi3  9471  oismo  9580  djuin  9958  updjudhcoinlf  9972  updjudhcoinrg  9973  acndom  10091  acndom2  10094  dfac12lem2  10185  dfac12lem3  10186  ackbij1  10277  cfflb  10299  fin23lem40  10391  fin23lem41  10392  isf34lem7  10419  fin1a2lem6  10445  fin1a2lem7  10446  hsmexlem4  10469  hsmexlem5  10470  axdc2lem  10488  axdc3lem2  10491  ttukeylem6  10554  unirnfdomd  10607  pwcfsdom  10623  smobeth  10626  pwfseqlem5  10703  tskurn  10829  wfgru  10856  rpnnen1lem4  13022  rpnnen1lem5  13023  unirnioo  13489  fseqsupcl  14018  fseqsupubi  14019  hashf1dmcdm  14483  limsupcl  15509  limsuple  15514  limsupval2  15516  prmreclem6  16959  0ram2  17059  0ramcl  17061  imasdsval2  17561  mrcssv  17657  isacs1i  17700  acsmapd  18599  acsmap2d  18600  gsumval1  18696  dfod2  19582  odcl2  19583  sylow1lem2  19617  efgsfo  19757  gexex  19871  iscyggen2  19899  iscyg3  19904  gsumval3lem1  19923  gsumval3  19925  dprdf1  20053  subgdmdprd  20054  subgdprd  20055  lindfmm  21847  m2cpmmhm  22751  leordtval2  23220  lecldbas  23227  discmp  23406  cmpsub  23408  tgcmp  23409  hauscmplem  23414  2ndcctbss  23463  2ndcsep  23467  comppfsc  23540  kgentop  23550  1stckgen  23562  kgencn2  23565  txuni2  23573  xkoopn  23597  xkouni  23607  xkoccn  23627  ptcnplem  23629  txkgen  23660  xkoco1cn  23665  xkoco2cn  23666  xkococnlem  23667  xkococn  23668  xkoinjcn  23695  hmphdis  23804  zfbas  23904  uzrest  23905  elfm  23955  alexsubALT  24059  efmndtmd  24109  submtmd  24112  symgtgp  24114  tsmsxplem1  24161  blin2  24439  imasf1oxms  24502  tgqioo  24821  xrtgioo  24828  metdscn2  24879  iimulcn  24967  iimulcnOLD  24968  icchmeo  24971  icchmeoOLD  24972  xrhmeo  24977  cnheiborlem  24986  tcphex  25251  tchnmfval  25262  fmcfil  25306  causs  25332  ovolficcss  25504  elovolm  25510  ovoliunlem2  25538  volsup  25591  uniioovol  25614  dyadmbllem  25634  dyadmbl  25635  opnmbllem  25636  opnmblALT  25638  volsup2  25640  mbfconstlem  25662  i1fd  25716  i1f1  25725  itg11  25726  itg1addlem4  25734  itg1climres  25749  itg2gt0  25795  limciun  25929  c1liplem1  26035  dvne0f1  26051  dvcnvrelem2  26057  dvcnvre  26058  mdeglt  26104  mdegxrcl  26106  mdegcl  26108  ig1peu  26214  ulmss  26440  reeff1o  26491  efifo  26589  dvlog  26693  efopn  26700  lgamcvg2  27098  dchrisum0fno1  27555  norn  27696  oldf  27896  usgredgss  29176  hhssims  31293  shsss  31332  pjrni  31721  imaelshi  32077  foresf1o  32523  fnpreimac  32681  tocyc01  33138  cycpmrn  33163  cycpmconjslem2  33175  cyc3conja  33177  dimkerim  33678  smatrcl  33795  locfinreflem  33839  esumcvg  34087  omssubadd  34302  sitgclbn  34345  eulerpartgbij  34374  eulerpartlemgvv  34378  eulerpartlemgf  34381  ballotlemsima  34518  lfuhgr  35123  mrsubf  35522  msubf  35537  mstapst  35552  mclsind  35575  mclsppslem  35588  icoreunrn  37360  pibt2  37418  ptrecube  37627  poimirlem1  37628  poimirlem3  37630  poimirlem12  37639  poimirlem16  37643  poimirlem32  37659  broucube  37661  heicant  37662  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  volsupnfl  37672  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  indexdom  37741  sstotbnd  37782  prdsbnd  37800  heibor1lem  37816  heiborlem1  37818  rrnval  37834  reheibor  37846  lsatset  38991  aks6d1c2  42131  aks6d1c6lem3  42173  aks6d1c6isolem1  42175  aks6d1c7lem1  42181  unitscyglem1  42196  elrfirn  42706  isnacs2  42717  nacsfix  42723  coeq0i  42764  diophrw  42770  dnwech  43060  pwssplit4  43101  hbt  43142  rnmptssf  45254  rnmptssff  45281  liminfval2  45783  fourierdlem12  46134  fourierdlem42  46164  fourierdlem54  46175  fourierdlem76  46197  fourierdlem85  46206  fourierdlem88  46209  fourierdlem93  46214  fourierdlem113  46234  hoicvr  46563  vonvolmbl2  46678  vonvol2  46679  fafvelcdm  47182  fafv2elcdm  47246  mgmplusfreseq  48081  elbigolo1  48478  aacllem  49320