Theorem frn 5966

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

Syntax hints:   → wi 4   ⊆ wss 3540  ran crn 5039   Fn wfn 5799  ⟶wf 5800

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 196  df-an 385  df-f 5808

This theorem is referenced by:  fco2  5972  fssxp  5973  fimass  5994  fimacnvdisj  5996  f00  6000  f0rn0  6003  foconst  6039  fimacnv  6255  ffvelrn  6265  f1ompt  6290  fnfvrnss  6297  rnmptss  6299  fliftrel  6458  isofr2  6494  fun11iun  7019  f1dmex  7029  fo1stres  7083  fo2ndres  7084  1stcof  7087  2ndcof  7088  fo2ndf  7171  fnwelem  7179  tposf2  7263  onoviun  7327  onnseq  7328  smores2  7338  seqomlem2  7433  oacomf1olem  7531  map0b  7782  mapsn  7785  f1imaen2g  7903  domdifsn  7928  domunsncan  7945  omxpenlem  7946  fodomr  7996  domss2  8004  f1finf1o  8072  f1fi  8136  unirnffid  8141  fipreima  8155  indexfi  8157  intrnfi  8205  dffi3  8220  ordtypelem8  8313  ordtypelem9  8314  ordtypelem10  8315  oismo  8328  hartogslem1  8330  brwdom2  8361  unxpwdom2  8376  ixpiunwdom  8379  infdifsn  8437  cantnf  8473  ac10ct  8740  numacn  8755  acndom  8757  acndom2  8760  infpwfien  8768  carduniima  8802  dfac12lem2  8849  dfac12lem3  8850  ackbij1  8943  fictb  8950  cfflb  8964  fin23lem40  9056  fin23lem41  9057  isf34lem5  9083  isf34lem7  9084  isf34lem6  9085  enfin1ai  9089  fin1a2lem6  9110  fin1a2lem7  9111  hsmexlem4  9134  hsmexlem5  9135  axdc2lem  9153  axdc3lem2  9156  ttukeylem6  9219  unirnfdomd  9268  pwcfsdom  9284  smobeth  9287  canthp1lem2  9354  pwfseqlem5  9364  wuncval2  9448  tskurn  9490  wfgru  9517  peano5nni  10900  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  unirnioo  12144  fseqsupcl  12638  fseqsupubi  12639  hashimarn  13085  hashf1lem1  13096  hashf1lem2  13097  ccatrn  13225  swrdrn  13281  cshwrn  13399  limsupcl  14052  limsupgle  14056  limsuple  14057  limsupval2  14059  limsupgre  14060  isercolllem2  14244  isercoll  14246  isercoll2  14247  climsup  14248  ruclem11  14808  prmreclem6  15463  4sqlem11  15497  vdwapf  15514  vdwlem11  15533  0ram  15562  0ram2  15563  0ramcl  15565  imasdsval2  15999  mrcssv  16097  isacs1i  16141  funcres2b  16380  funcres2c  16384  setcepi  16561  yoniso  16748  isacs4lem  16991  acsmapd  17001  acsmap2d  17002  gsumval1  17100  mhmima  17186  gsumwspan  17206  frmdss2  17223  cycsubgcl  17443  cycsubgss  17444  ghmrn  17496  conjnmz  17517  cntzmhm  17594  f1omvdconj  17689  psgnunilem1  17736  dfod2  17804  odcl2  17805  odf1o2  17811  sylow1lem2  17837  pgpssslw  17852  sylow2blem1  17858  lsmssv  17881  lsmidm  17900  pj1ghm2  17940  efgsp1  17973  efgsfo  17975  efgrelexlemb  17986  cntzcmnf  18071  gexex  18079  iscyggen2  18106  cyggenod  18109  iscyg3  18111  gsumval3eu  18128  gsumval3lem1  18129  gsumval3lem2  18130  gsumval3  18131  gsumzsubmcl  18141  gsumzaddlem  18144  gsumzadd  18145  gsumzsplit  18150  gsumconst  18157  gsumzoppg  18167  gsumpt  18184  dmdprdd  18221  dprdfcntz  18237  dprdfeq0  18244  dprdlub  18248  dprdres  18250  dprdss  18251  dprdz  18252  dprdf1  18255  subgdmdprd  18256  subgdprd  18257  dprd2dlem1  18263  dprd2da  18264  dmdprdsplit2lem  18267  dpjghm2  18286  ablfac1b  18292  lmhmlsp  18870  pj1lmhm2  18922  aspval2  19168  mplcoe5lem  19288  mplbas2  19291  mplind  19323  evlslem1  19336  evlseu  19337  gsumply1subr  19425  pjfo  19878  frlmsplit2  19931  frlmsslsp  19954  frlmlbs  19955  frlmup3  19958  frlmup4  19959  lindff1  19978  lindfrn  19979  f1lindf  19980  lindfmm  19985  indlcim  19998  m2cpmf1  20367  m2cpmghm  20368  m2cpmmhm  20369  iinopn  20532  pptbas  20622  tgrest  20773  resttopon  20775  rest0  20783  restfpw  20793  ordtbaslem  20802  ordtuni  20804  ordtbas2  20805  ordtrest  20816  ordtrest2  20818  leordtval2  20826  lecldbas  20833  cnclsi  20886  cnrest2r  20901  cnprest2  20904  lmss  20912  cncmp  21005  rncmp  21009  discmp  21011  cmpsub  21013  tgcmp  21014  hauscmplem  21019  conima  21038  concn  21039  2ndcctbss  21068  2ndcdisj  21069  2ndcomap  21071  2ndcsep  21072  dis2ndc  21073  lly1stc  21109  comppfsc  21145  kgentop  21155  kgencmp  21158  1stckgenlem  21166  1stckgen  21167  kgencn2  21170  kgencn3  21171  txuni2  21178  ptbasfi  21194  xkoopn  21202  xkouni  21212  txbasval  21219  xkoccn  21232  ptcnplem  21234  upxp  21236  uptx  21238  txtube  21253  txcmplem1  21254  txcmplem2  21255  tx1stc  21263  txkgen  21265  xkoptsub  21267  xkoco1cn  21270  xkoco2cn  21271  xkococnlem  21272  xkococn  21273  xkoinjcn  21300  hmeores  21384  hmphdis  21409  fbasrn  21498  trfilss  21503  trfg  21505  zfbas  21510  uzrest  21511  elfm  21561  imaelfm  21565  rnelfmlem  21566  fclscmpi  21643  alexsublem  21658  alexsubALT  21665  ptcmplem1  21666  ptcmplem3  21668  cnextcn  21681  tmdgsum2  21710  symgtgp  21715  submtmd  21718  subgtgp  21719  subgntr  21720  opnsubg  21721  clsnsg  21723  tgpconcomp  21726  tsmsfbas  21741  tsmsxplem1  21766  prdsdsf  21982  prdsxmetlem  21983  prdsmet  21985  imasdsf1olem  21988  unirnblps  22034  unirnbl  22035  blin2  22044  imasf1oxms  22104  prdsbl  22106  met1stc  22136  met2ndci  22137  prdsxmslem2  22144  tgqioo  22411  xrtgioo  22417  xrge0gsumle  22444  xrge0tsms  22445  metdcn2  22450  metdsf  22459  metdsge  22460  metdscn2  22468  cnmptre  22534  iimulcn  22545  icchmeo  22548  xrhmeo  22553  cnheiborlem  22561  bndth  22565  evth  22566  evth2  22567  lebnumlem2  22569  lebnumlem3  22570  reparphti  22605  tchex  22824  tchnmfval  22835  fmcfil  22878  causs  22904  bcthlem5  22933  minveclem1  23003  minveclem3b  23007  evthicc2  23036  ovolficcss  23045  elovolm  23050  ovolmge0  23052  ovollb  23054  ovolgelb  23055  ovollb2lem  23063  ovollb2  23064  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovoliun  23080  ovoliun2  23081  ovolscalem1  23088  ovolicc1  23091  ovolicc2lem4  23095  ovolicc2  23097  voliunlem2  23126  voliunlem3  23127  volsup  23131  ioombl1lem2  23134  ioombl1lem4  23136  uniioovol  23153  uniiccvol  23154  uniioombllem1  23155  uniioombllem2  23157  uniioombllem3  23159  uniioombllem6  23162  uniioombl  23163  dyadmbllem  23173  dyadmbl  23174  opnmbllem  23175  opnmblALT  23177  volsup2  23179  vitalilem2  23184  vitalilem4  23186  vitalilem5  23187  mbfconstlem  23202  mbfsup  23237  mbfinf  23238  mbflimsup  23239  i1fima  23251  i1fima2  23252  i1fd  23254  itg1cl  23258  itg1ge0  23259  i1f1  23263  itg11  23264  i1fmullem  23267  i1fadd  23268  i1fmul  23269  itg1addlem4  23272  itg1addlem5  23273  i1fmulc  23276  itg1mulc  23277  i1fres  23278  itg10a  23283  itg1ge0a  23284  itg1climres  23287  mbfi1fseqlem4  23291  itg2seq  23315  itg2monolem1  23323  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  itg2i1fseq2  23329  itg2gt0  23333  itg2cnlem1  23334  itg2cn  23336  limciun  23464  c1liplem1  23563  dvne0  23578  dvne0f1  23579  lhop2  23582  dvcnvrelem2  23585  dvcnvre  23586  mdegleb  23628  mdeglt  23629  mdegldg  23630  mdegxrcl  23631  mdegcl  23633  ig1peu  23735  aalioulem3  23893  ulmss  23955  reeff1o  24005  efifo  24097  dvlog  24197  efopn  24204  logccv  24209  efrlim  24496  lgamcvg2  24581  basellem3  24609  fsumvma  24738  lgseisenlem4  24903  dchrisum0fno1  25000  uhgredgn0  25802  upgredgss  25806  umgredgss  25807  edgupgr  25808  upgredg  25811  edgss  25881  frgrancvvdeqlem8  26567  ubthlem1  27110  minvecolem1  27114  htthlem  27158  hhssims  27516  shsss  27556  pjrni  27945  imaelshi  28301  foresf1o  28727  ofrn  28821  ofrn2  28822  fimarab  28825  xppreima2  28830  xrge0tsmsd  29116  smatrcl  29190  locfinreflem  29235  cmpcref  29245  ordtrestNEW  29295  ordtrest2NEW  29297  xrge0mulc1cn  29315  rge0scvg  29323  esumcst  29452  esumpfinvallem  29463  esumpcvgval  29467  esumcvg  29475  esumiun  29483  omssubadd  29689  carsggect  29707  sibfinima  29728  sitgclg  29731  sitgclbn  29732  sitgaddlemb  29737  eulerpartgbij  29761  eulerpartlemgvv  29765  eulerpartlemgf  29768  rrvrnss  29836  orvcval4  29849  ballotlemsima  29904  erdsze2lem2  30440  cvxpcon  30478  cvxscon  30479  cvmsss2  30510  cvmliftlem8  30528  cvmlift3lem6  30560  mrsubrn  30664  mrsubf  30668  msubrn  30680  msubf  30683  mstapst  30698  mvtss  30704  mclsssvlem  30713  mclsax  30720  mclsind  30721  mclsppslem  30734  orderseqlem  30993  norn  31048  neibastop2lem  31525  tailfb  31542  knoppcnlem10  31662  icoreunrn  32383  lindsdom  32573  ptrecube  32579  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem19  32598  poimirlem27  32606  poimirlem30  32609  poimirlem32  32611  broucube  32613  heicant  32614  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  volsupnfl  32624  itg2addnclem2  32632  itg2gt0cn  32635  ftc1anclem3  32657  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  indexdom  32699  cnresima  32733  istotbnd3  32740  sstotbnd2  32743  sstotbnd  32744  totbndbnd  32758  prdsbnd  32762  cntotbnd  32765  ismtyima  32772  heibor1lem  32778  heiborlem1  32780  heibor  32790  rrnval  32796  rrnequiv  32804  reheibor  32808  lsatset  33295  lsatlss  33301  cdleme50rnlem  34850  elrfirn  36276  cmpfiiin  36278  isnacs2  36287  isnacs3  36291  nacsfix  36293  coeq0i  36334  diophrw  36340  eldioph2lem2  36342  dnwech  36636  fnwe2lem2  36639  lmhmfgima  36672  pwssplit4  36677  hbt  36719  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  refsumcn  38212  cncmpmax  38214  mapsnd  38383  elpmrn  38409  frnd  38421  climinf  38673  icccncfext  38773  dvsinax  38801  itgsubsticclem  38867  fourierdlem12  39012  fourierdlem42  39042  fourierdlem54  39053  fourierdlem70  39069  fourierdlem76  39075  fourierdlem82  39081  fourierdlem85  39084  fourierdlem88  39087  fourierdlem93  39092  fourierdlem113  39112  fge0npnf  39260  sge0resrnlem  39296  sge0isum  39320  sge0seq  39339  meadjiunlem  39358  omeiunle  39407  hoicvr  39438  vonvolmbllem  39550  vonvolmbl2  39553  vonvol2  39554  fafvelrn  39899  pfxrn  40256  usgredgss  40390  usgruspgrb  40411  upgrres1  40532  frgrncvvdeqlem8  41479  mgmplusfreseq  41563  mgmhmima  41592  elbigolo1  42149  aacllem  42356