Theorem frn 6605

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

Syntax hints:   → wi 4   ⊆ wss 3892  ran crn 5591   Fn wfn 6427  ⟶wf 6428

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 397  df-f 6436

This theorem is referenced by:  frnd  6606  fimass  6619  fimacnv  6620  fco2  6625  fssxp  6626  fimacnvdisj  6650  f00  6654  f0rn0  6657  f1resf1  6677  foconst  6701  ffvelrn  6956  f1ompt  6982  fnfvrnss  6991  rnmptss  6993  isofr2  7211  fiun  7779  fo1stres  7850  fo2ndres  7851  1stcof  7854  2ndcof  7855  fnwelem  7963  tposf2  8057  seqomlem2  8273  oacomf1olem  8380  map0b  8654  mapsnd  8657  fipreima  9103  indexfi  9105  dffi3  9168  oismo  9277  djuin  9677  updjudhcoinlf  9691  updjudhcoinrg  9692  acndom  9808  acndom2  9811  dfac12lem2  9901  dfac12lem3  9902  ackbij1  9995  cfflb  10016  fin23lem40  10108  fin23lem41  10109  isf34lem7  10136  fin1a2lem6  10162  fin1a2lem7  10163  hsmexlem4  10186  hsmexlem5  10187  axdc2lem  10205  axdc3lem2  10208  ttukeylem6  10271  unirnfdomd  10324  pwcfsdom  10340  smobeth  10343  pwfseqlem5  10420  tskurn  10546  wfgru  10573  rpnnen1lem4  12719  rpnnen1lem5  12720  unirnioo  13180  fseqsupcl  13695  fseqsupubi  13696  limsupcl  15180  limsuple  15185  limsupval2  15187  prmreclem6  16620  0ram2  16720  0ramcl  16722  imasdsval2  17225  mrcssv  17321  isacs1i  17364  acsmapd  18270  acsmap2d  18271  gsumval1  18365  dfod2  19169  odcl2  19170  sylow1lem2  19202  efgsfo  19343  gexex  19452  iscyggen2  19479  iscyg3  19484  gsumval3lem1  19504  gsumval3  19506  dprdf1  19634  subgdmdprd  19635  subgdprd  19636  lindfmm  21032  m2cpmmhm  21892  leordtval2  22361  lecldbas  22368  discmp  22547  cmpsub  22549  tgcmp  22550  hauscmplem  22555  2ndcctbss  22604  2ndcsep  22608  comppfsc  22681  kgentop  22691  1stckgen  22703  kgencn2  22706  txuni2  22714  xkoopn  22738  xkouni  22748  xkoccn  22768  ptcnplem  22770  txkgen  22801  xkoco1cn  22806  xkoco2cn  22807  xkococnlem  22808  xkococn  22809  xkoinjcn  22836  hmphdis  22945  zfbas  23045  uzrest  23046  elfm  23096  alexsubALT  23200  efmndtmd  23250  submtmd  23253  symgtgp  23255  tsmsxplem1  23302  blin2  23580  imasf1oxms  23643  tgqioo  23961  xrtgioo  23967  metdscn2  24018  iimulcn  24099  icchmeo  24102  xrhmeo  24107  cnheiborlem  24115  tcphex  24379  tchnmfval  24390  fmcfil  24434  causs  24460  ovolficcss  24631  elovolm  24637  ovoliunlem2  24665  volsup  24718  uniioovol  24741  dyadmbllem  24761  dyadmbl  24762  opnmbllem  24763  opnmblALT  24765  volsup2  24767  mbfconstlem  24789  i1fd  24843  i1f1  24852  itg11  24853  itg1addlem4  24861  itg1addlem4OLD  24862  itg1climres  24877  itg2gt0  24923  limciun  25056  c1liplem1  25158  dvne0f1  25174  dvcnvrelem2  25180  dvcnvre  25181  mdeglt  25228  mdegxrcl  25230  mdegcl  25232  ig1peu  25334  ulmss  25554  reeff1o  25604  efifo  25701  dvlog  25804  efopn  25811  lgamcvg2  26202  dchrisum0fno1  26657  usgredgss  27527  hhssims  29632  shsss  29671  pjrni  30060  imaelshi  30416  foresf1o  30846  fnpreimac  31004  tocyc01  31381  cycpmrn  31406  cycpmconjslem2  31418  cyc3conja  31420  dimkerim  31704  smatrcl  31742  locfinreflem  31786  esumcvg  32050  omssubadd  32263  sitgclbn  32306  eulerpartgbij  32335  eulerpartlemgvv  32339  eulerpartlemgf  32342  ballotlemsima  32478  hashf1dmcdm  33072  lfuhgr  33075  mrsubf  33475  msubf  33490  mstapst  33505  mclsind  33528  mclsppslem  33541  orderseqlem  33797  norn  33850  oldf  34037  icoreunrn  35526  pibt2  35584  ptrecube  35773  poimirlem1  35774  poimirlem3  35776  poimirlem12  35785  poimirlem16  35789  poimirlem32  35805  broucube  35807  heicant  35808  opnmbllem0  35809  mblfinlem1  35810  mblfinlem2  35811  mblfinlem3  35812  mblfinlem4  35813  ismblfin  35814  volsupnfl  35818  ftc1anclem5  35850  ftc1anclem7  35852  ftc1anclem8  35853  ftc1anc  35854  indexdom  35888  sstotbnd  35929  prdsbnd  35947  heibor1lem  35963  heiborlem1  35965  rrnval  35981  reheibor  35993  lsatset  37000  elrfirn  40514  isnacs2  40525  nacsfix  40531  coeq0i  40572  diophrw  40578  dnwech  40870  pwssplit4  40911  hbt  40952  rnmptssf  42763  liminfval2  43280  fourierdlem12  43631  fourierdlem42  43661  fourierdlem54  43672  fourierdlem76  43694  fourierdlem85  43703  fourierdlem88  43706  fourierdlem93  43711  fourierdlem113  43731  hoicvr  44057  vonvolmbl2  44172  vonvol2  44173  fafvelrn  44630  fafv2elrn  44694  mgmplusfreseq  45296  elbigolo1  45872  aacllem  46474