Theorem frn 6725

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

Syntax hints:   → wi 4   ⊆ wss 3949  ran crn 5678   Fn wfn 6539  ⟶wf 6540

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 206  df-an 398  df-f 6548

This theorem is referenced by:  frnd  6726  fimass  6739  fimacnv  6740  fco2  6745  fssxp  6746  fimacnvdisj  6770  f00  6774  f0rn0  6777  f1resf1  6797  foconst  6821  ffvelcdm  7084  f1ompt  7111  fnfvrnss  7120  rnmptss  7122  isofr2  7341  fiun  7929  fo1stres  8001  fo2ndres  8002  1stcof  8005  2ndcof  8006  fnwelem  8117  orderseqlem  8143  tposf2  8235  seqomlem2  8451  oacomf1olem  8564  naddunif  8692  naddasslem1  8693  naddasslem2  8694  map0b  8877  mapsnd  8880  fipreima  9358  indexfi  9360  dffi3  9426  oismo  9535  djuin  9913  updjudhcoinlf  9927  updjudhcoinrg  9928  acndom  10046  acndom2  10049  dfac12lem2  10139  dfac12lem3  10140  ackbij1  10233  cfflb  10254  fin23lem40  10346  fin23lem41  10347  isf34lem7  10374  fin1a2lem6  10400  fin1a2lem7  10401  hsmexlem4  10424  hsmexlem5  10425  axdc2lem  10443  axdc3lem2  10446  ttukeylem6  10509  unirnfdomd  10562  pwcfsdom  10578  smobeth  10581  pwfseqlem5  10658  tskurn  10784  wfgru  10811  rpnnen1lem4  12964  rpnnen1lem5  12965  unirnioo  13426  fseqsupcl  13942  fseqsupubi  13943  limsupcl  15417  limsuple  15422  limsupval2  15424  prmreclem6  16854  0ram2  16954  0ramcl  16956  imasdsval2  17462  mrcssv  17558  isacs1i  17601  acsmapd  18507  acsmap2d  18508  gsumval1  18602  dfod2  19432  odcl2  19433  sylow1lem2  19467  efgsfo  19607  gexex  19721  iscyggen2  19749  iscyg3  19754  gsumval3lem1  19773  gsumval3  19775  dprdf1  19903  subgdmdprd  19904  subgdprd  19905  lindfmm  21382  m2cpmmhm  22247  leordtval2  22716  lecldbas  22723  discmp  22902  cmpsub  22904  tgcmp  22905  hauscmplem  22910  2ndcctbss  22959  2ndcsep  22963  comppfsc  23036  kgentop  23046  1stckgen  23058  kgencn2  23061  txuni2  23069  xkoopn  23093  xkouni  23103  xkoccn  23123  ptcnplem  23125  txkgen  23156  xkoco1cn  23161  xkoco2cn  23162  xkococnlem  23163  xkococn  23164  xkoinjcn  23191  hmphdis  23300  zfbas  23400  uzrest  23401  elfm  23451  alexsubALT  23555  efmndtmd  23605  submtmd  23608  symgtgp  23610  tsmsxplem1  23657  blin2  23935  imasf1oxms  23998  tgqioo  24316  xrtgioo  24322  metdscn2  24373  iimulcn  24454  icchmeo  24457  xrhmeo  24462  cnheiborlem  24470  tcphex  24734  tchnmfval  24745  fmcfil  24789  causs  24815  ovolficcss  24986  elovolm  24992  ovoliunlem2  25020  volsup  25073  uniioovol  25096  dyadmbllem  25116  dyadmbl  25117  opnmbllem  25118  opnmblALT  25120  volsup2  25122  mbfconstlem  25144  i1fd  25198  i1f1  25207  itg11  25208  itg1addlem4  25216  itg1addlem4OLD  25217  itg1climres  25232  itg2gt0  25278  limciun  25411  c1liplem1  25513  dvne0f1  25529  dvcnvrelem2  25535  dvcnvre  25536  mdeglt  25583  mdegxrcl  25585  mdegcl  25587  ig1peu  25689  ulmss  25909  reeff1o  25959  efifo  26056  dvlog  26159  efopn  26166  lgamcvg2  26559  dchrisum0fno1  27014  norn  27154  oldf  27352  usgredgss  28419  hhssims  30527  shsss  30566  pjrni  30955  imaelshi  31311  foresf1o  31742  fnpreimac  31896  tocyc01  32277  cycpmrn  32302  cycpmconjslem2  32314  cyc3conja  32316  dimkerim  32712  smatrcl  32776  locfinreflem  32820  esumcvg  33084  omssubadd  33299  sitgclbn  33342  eulerpartgbij  33371  eulerpartlemgvv  33375  eulerpartlemgf  33378  ballotlemsima  33514  hashf1dmcdm  34105  lfuhgr  34108  mrsubf  34508  msubf  34523  mstapst  34538  mclsind  34561  mclsppslem  34574  gg-iimulcn  35169  gg-icchmeo  35170  icoreunrn  36240  pibt2  36298  ptrecube  36488  poimirlem1  36489  poimirlem3  36491  poimirlem12  36500  poimirlem16  36504  poimirlem32  36520  broucube  36522  heicant  36523  opnmbllem0  36524  mblfinlem1  36525  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  volsupnfl  36533  ftc1anclem5  36565  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  indexdom  36602  sstotbnd  36643  prdsbnd  36661  heibor1lem  36677  heiborlem1  36679  rrnval  36695  reheibor  36707  lsatset  37860  elrfirn  41433  isnacs2  41444  nacsfix  41450  coeq0i  41491  diophrw  41497  dnwech  41790  pwssplit4  41831  hbt  41872  rnmptssf  43951  rnmptssff  43979  liminfval2  44484  fourierdlem12  44835  fourierdlem42  44865  fourierdlem54  44876  fourierdlem76  44898  fourierdlem85  44907  fourierdlem88  44910  fourierdlem93  44915  fourierdlem113  44935  hoicvr  45264  vonvolmbl2  45379  vonvol2  45380  fafvelcdm  45878  fafv2elcdm  45942  mgmplusfreseq  46543  elbigolo1  47243  aacllem  47848