Theorem frn 6677

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

Syntax hints:   → wi 4   ⊆ wss 3911  ran crn 5632   Fn wfn 6494  ⟶wf 6495

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 6503

This theorem is referenced by:  frnd  6678  fimass  6690  fimacnv  6692  fco2  6696  fssxp  6697  fimacnvdisj  6720  f00  6724  f0rn0  6727  f1resf1  6746  foconst  6769  ffvelcdm  7035  f1ompt  7065  fnfvrnss  7075  rnmptss  7077  isofr2  7301  fiun  7901  fo1stres  7973  fo2ndres  7974  1stcof  7977  2ndcof  7978  fnwelem  8087  orderseqlem  8113  tposf2  8206  seqomlem2  8396  oacomf1olem  8505  naddunif  8634  naddasslem1  8635  naddasslem2  8636  map0b  8833  mapsnd  8836  fipreima  9285  indexfi  9287  dffi3  9358  oismo  9469  djuin  9847  updjudhcoinlf  9861  updjudhcoinrg  9862  acndom  9980  acndom2  9983  dfac12lem2  10074  dfac12lem3  10075  ackbij1  10166  cfflb  10188  fin23lem40  10280  fin23lem41  10281  isf34lem7  10308  fin1a2lem6  10334  fin1a2lem7  10335  hsmexlem4  10358  hsmexlem5  10359  axdc2lem  10377  axdc3lem2  10380  ttukeylem6  10443  unirnfdomd  10496  pwcfsdom  10512  smobeth  10515  pwfseqlem5  10592  tskurn  10718  wfgru  10745  rpnnen1lem4  12915  rpnnen1lem5  12916  unirnioo  13386  fseqsupcl  13918  fseqsupubi  13919  hashf1dmcdm  14385  limsupcl  15415  limsuple  15420  limsupval2  15422  prmreclem6  16868  0ram2  16968  0ramcl  16970  imasdsval2  17455  mrcssv  17555  isacs1i  17598  acsmapd  18495  acsmap2d  18496  gsumval1  18592  dfod2  19478  odcl2  19479  sylow1lem2  19513  efgsfo  19653  gexex  19767  iscyggen2  19795  iscyg3  19800  gsumval3lem1  19819  gsumval3  19821  dprdf1  19949  subgdmdprd  19950  subgdprd  19951  lindfmm  21769  m2cpmmhm  22665  leordtval2  23132  lecldbas  23139  discmp  23318  cmpsub  23320  tgcmp  23321  hauscmplem  23326  2ndcctbss  23375  2ndcsep  23379  comppfsc  23452  kgentop  23462  1stckgen  23474  kgencn2  23477  txuni2  23485  xkoopn  23509  xkouni  23519  xkoccn  23539  ptcnplem  23541  txkgen  23572  xkoco1cn  23577  xkoco2cn  23578  xkococnlem  23579  xkococn  23580  xkoinjcn  23607  hmphdis  23716  zfbas  23816  uzrest  23817  elfm  23867  alexsubALT  23971  efmndtmd  24021  submtmd  24024  symgtgp  24026  tsmsxplem1  24073  blin2  24350  imasf1oxms  24410  tgqioo  24721  xrtgioo  24728  metdscn2  24779  iimulcn  24867  iimulcnOLD  24868  icchmeo  24871  icchmeoOLD  24872  xrhmeo  24877  cnheiborlem  24886  tcphex  25150  tchnmfval  25161  fmcfil  25205  causs  25231  ovolficcss  25403  elovolm  25409  ovoliunlem2  25437  volsup  25490  uniioovol  25513  dyadmbllem  25533  dyadmbl  25534  opnmbllem  25535  opnmblALT  25537  volsup2  25539  mbfconstlem  25561  i1fd  25615  i1f1  25624  itg11  25625  itg1addlem4  25633  itg1climres  25648  itg2gt0  25694  limciun  25828  c1liplem1  25934  dvne0f1  25950  dvcnvrelem2  25956  dvcnvre  25957  mdeglt  26003  mdegxrcl  26005  mdegcl  26007  ig1peu  26113  ulmss  26339  reeff1o  26390  efifo  26489  dvlog  26593  efopn  26600  lgamcvg2  26998  dchrisum0fno1  27455  norn  27596  oldf  27802  usgredgss  29139  hhssims  31253  shsss  31292  pjrni  31681  imaelshi  32037  foresf1o  32483  fnpreimac  32645  tocyc01  33090  cycpmrn  33115  cycpmconjslem2  33127  cyc3conja  33129  dimkerim  33616  smatrcl  33779  locfinreflem  33823  esumcvg  34069  omssubadd  34284  sitgclbn  34327  eulerpartgbij  34356  eulerpartlemgvv  34360  eulerpartlemgf  34363  ballotlemsima  34500  lfuhgr  35098  mrsubf  35497  msubf  35512  mstapst  35527  mclsind  35550  mclsppslem  35563  icoreunrn  37340  pibt2  37398  ptrecube  37607  poimirlem1  37608  poimirlem3  37610  poimirlem12  37619  poimirlem16  37623  poimirlem32  37639  broucube  37641  heicant  37642  opnmbllem0  37643  mblfinlem1  37644  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  volsupnfl  37652  ftc1anclem5  37684  ftc1anclem7  37686  ftc1anclem8  37687  ftc1anc  37688  indexdom  37721  sstotbnd  37762  prdsbnd  37780  heibor1lem  37796  heiborlem1  37798  rrnval  37814  reheibor  37826  lsatset  38976  aks6d1c2  42111  aks6d1c6lem3  42153  aks6d1c6isolem1  42155  aks6d1c7lem1  42161  unitscyglem1  42176  elrfirn  42676  isnacs2  42687  nacsfix  42693  coeq0i  42734  diophrw  42740  dnwech  43030  pwssplit4  43071  hbt  43112  rnmptssf  45234  rnmptssff  45261  liminfval2  45759  fourierdlem12  46110  fourierdlem42  46140  fourierdlem54  46151  fourierdlem76  46173  fourierdlem85  46182  fourierdlem88  46185  fourierdlem93  46190  fourierdlem113  46210  hoicvr  46539  vonvolmbl2  46654  vonvol2  46655  fafvelcdm  47164  fafv2elcdm  47228  mgmplusfreseq  48146  elbigolo1  48539  aacllem  49783