Theorem frn 6493

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

Syntax hints:   → wi 4   ⊆ wss 3881  ran crn 5520   Fn wfn 6319  ⟶wf 6320

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 210  df-an 400  df-f 6328

This theorem is referenced by:  frnd  6494  fco2  6507  fssxp  6508  fimass  6529  fimacnvdisj  6531  f00  6535  f0rn0  6538  f1resf1  6558  foconst  6578  ffvelrn  6826  f1ompt  6852  fnfvrnss  6861  rnmptss  6863  isofr2  7076  fiun  7626  fo1stres  7697  fo2ndres  7698  1stcof  7701  2ndcof  7702  fnwelem  7808  tposf2  7899  seqomlem2  8070  oacomf1olem  8173  map0b  8430  mapsnd  8433  fipreima  8814  indexfi  8816  dffi3  8879  oismo  8988  djuin  9331  updjudhcoinlf  9345  updjudhcoinrg  9346  acndom  9462  acndom2  9465  dfac12lem2  9555  dfac12lem3  9556  ackbij1  9649  cfflb  9670  fin23lem40  9762  fin23lem41  9763  isf34lem7  9790  fin1a2lem6  9816  fin1a2lem7  9817  hsmexlem4  9840  hsmexlem5  9841  axdc2lem  9859  axdc3lem2  9862  ttukeylem6  9925  unirnfdomd  9978  pwcfsdom  9994  smobeth  9997  pwfseqlem5  10074  tskurn  10200  wfgru  10227  rpnnen1lem4  12367  rpnnen1lem5  12368  unirnioo  12827  fseqsupcl  13340  fseqsupubi  13341  limsupcl  14822  limsuple  14827  limsupval2  14829  prmreclem6  16247  0ram2  16347  0ramcl  16349  imasdsval2  16781  mrcssv  16877  isacs1i  16920  acsmapd  17780  acsmap2d  17781  gsumval1  17885  dfod2  18683  odcl2  18684  sylow1lem2  18716  efgsfo  18857  gexex  18966  iscyggen2  18993  iscyg3  18998  gsumval3lem1  19018  gsumval3  19020  dprdf1  19148  subgdmdprd  19149  subgdprd  19150  lindfmm  20516  m2cpmmhm  21350  leordtval2  21817  lecldbas  21824  discmp  22003  cmpsub  22005  tgcmp  22006  hauscmplem  22011  2ndcctbss  22060  2ndcsep  22064  comppfsc  22137  kgentop  22147  1stckgen  22159  kgencn2  22162  txuni2  22170  xkoopn  22194  xkouni  22204  xkoccn  22224  ptcnplem  22226  txkgen  22257  xkoco1cn  22262  xkoco2cn  22263  xkococnlem  22264  xkococn  22265  xkoinjcn  22292  hmphdis  22401  zfbas  22501  uzrest  22502  elfm  22552  alexsubALT  22656  efmndtmd  22706  submtmd  22709  symgtgp  22711  tsmsxplem1  22758  blin2  23036  imasf1oxms  23096  tgqioo  23405  xrtgioo  23411  metdscn2  23462  iimulcn  23543  icchmeo  23546  xrhmeo  23551  cnheiborlem  23559  tcphex  23821  tchnmfval  23832  fmcfil  23876  causs  23902  ovolficcss  24073  elovolm  24079  ovoliunlem2  24107  volsup  24160  uniioovol  24183  dyadmbllem  24203  dyadmbl  24204  opnmbllem  24205  opnmblALT  24207  volsup2  24209  mbfconstlem  24231  i1fd  24285  i1f1  24294  itg11  24295  itg1addlem4  24303  itg1climres  24318  itg2gt0  24364  limciun  24497  c1liplem1  24599  dvne0f1  24615  dvcnvrelem2  24621  dvcnvre  24622  mdeglt  24666  mdegxrcl  24668  mdegcl  24670  ig1peu  24772  ulmss  24992  reeff1o  25042  efifo  25139  dvlog  25242  efopn  25249  lgamcvg2  25640  dchrisum0fno1  26095  usgredgss  26952  hhssims  29057  shsss  29096  pjrni  29485  imaelshi  29841  foresf1o  30273  fnpreimac  30434  tocyc01  30810  cycpmrn  30835  cycpmconjslem2  30847  cyc3conja  30849  dimkerim  31111  smatrcl  31149  locfinreflem  31193  esumcvg  31455  omssubadd  31668  sitgclbn  31711  eulerpartgbij  31740  eulerpartlemgvv  31744  eulerpartlemgf  31747  ballotlemsima  31883  hashf1dmcdm  32466  lfuhgr  32477  mrsubf  32877  msubf  32892  mstapst  32907  mclsind  32930  mclsppslem  32943  orderseqlem  33207  norn  33271  icoreunrn  34776  pibt2  34834  ptrecube  35057  poimirlem1  35058  poimirlem3  35060  poimirlem12  35069  poimirlem16  35073  poimirlem32  35089  broucube  35091  heicant  35092  opnmbllem0  35093  mblfinlem1  35094  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  volsupnfl  35102  ftc1anclem5  35134  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  indexdom  35172  sstotbnd  35213  prdsbnd  35231  heibor1lem  35247  heiborlem1  35249  rrnval  35265  reheibor  35277  lsatset  36286  elrfirn  39636  isnacs2  39647  nacsfix  39653  coeq0i  39694  diophrw  39700  dnwech  39992  pwssplit4  40033  hbt  40074  rnmptssf  41885  liminfval2  42410  fourierdlem12  42761  fourierdlem42  42791  fourierdlem54  42802  fourierdlem76  42824  fourierdlem85  42833  fourierdlem88  42836  fourierdlem93  42841  fourierdlem113  42861  hoicvr  43187  vonvolmbl2  43302  vonvol2  43303  fafvelrn  43726  fafv2elrn  43790  mgmplusfreseq  44393  elbigolo1  44971  aacllem  45329