Theorem frn 6520

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

Syntax hints:   → wi 4   ⊆ wss 3936  ran crn 5556   Fn wfn 6350  ⟶wf 6351

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 209  df-an 399  df-f 6359

This theorem is referenced by:  frnd  6521  fco2  6533  fssxp  6534  fimass  6555  fimacnvdisj  6557  f00  6561  f0rn0  6564  f1resf1  6583  foconst  6603  ffvelrn  6849  f1ompt  6875  fnfvrnss  6884  rnmptss  6886  isofr2  7097  fiun  7644  fo1stres  7715  fo2ndres  7716  1stcof  7719  2ndcof  7720  fnwelem  7825  tposf2  7916  seqomlem2  8087  oacomf1olem  8190  map0b  8447  mapsnd  8450  fipreima  8830  indexfi  8832  dffi3  8895  oismo  9004  djuin  9347  updjudhcoinlf  9361  updjudhcoinrg  9362  acndom  9477  acndom2  9480  dfac12lem2  9570  dfac12lem3  9571  ackbij1  9660  cfflb  9681  fin23lem40  9773  fin23lem41  9774  isf34lem7  9801  fin1a2lem6  9827  fin1a2lem7  9828  hsmexlem4  9851  hsmexlem5  9852  axdc2lem  9870  axdc3lem2  9873  ttukeylem6  9936  unirnfdomd  9989  pwcfsdom  10005  smobeth  10008  pwfseqlem5  10085  tskurn  10211  wfgru  10238  rpnnen1lem4  12380  rpnnen1lem5  12381  unirnioo  12838  fseqsupcl  13346  fseqsupubi  13347  limsupcl  14830  limsuple  14835  limsupval2  14837  prmreclem6  16257  0ram2  16357  0ramcl  16359  imasdsval2  16789  mrcssv  16885  isacs1i  16928  acsmapd  17788  acsmap2d  17789  gsumval1  17893  dfod2  18691  odcl2  18692  sylow1lem2  18724  efgsfo  18865  gexex  18973  iscyggen2  19000  iscyg3  19005  gsumval3lem1  19025  gsumval3  19027  dprdf1  19155  subgdmdprd  19156  subgdprd  19157  lindfmm  20971  m2cpmmhm  21353  leordtval2  21820  lecldbas  21827  discmp  22006  cmpsub  22008  tgcmp  22009  hauscmplem  22014  2ndcctbss  22063  2ndcsep  22067  comppfsc  22140  kgentop  22150  1stckgen  22162  kgencn2  22165  txuni2  22173  xkoopn  22197  xkouni  22207  xkoccn  22227  ptcnplem  22229  txkgen  22260  xkoco1cn  22265  xkoco2cn  22266  xkococnlem  22267  xkococn  22268  xkoinjcn  22295  hmphdis  22404  zfbas  22504  uzrest  22505  elfm  22555  alexsubALT  22659  efmndtmd  22709  submtmd  22712  symgtgp  22714  tsmsxplem1  22761  blin2  23039  imasf1oxms  23099  tgqioo  23408  xrtgioo  23414  metdscn2  23465  iimulcn  23542  icchmeo  23545  xrhmeo  23550  cnheiborlem  23558  tcphex  23820  tchnmfval  23831  fmcfil  23875  causs  23901  ovolficcss  24070  elovolm  24076  ovoliunlem2  24104  volsup  24157  uniioovol  24180  dyadmbllem  24200  dyadmbl  24201  opnmbllem  24202  opnmblALT  24204  volsup2  24206  mbfconstlem  24228  i1fd  24282  i1f1  24291  itg11  24292  itg1addlem4  24300  itg1climres  24315  itg2gt0  24361  limciun  24492  c1liplem1  24593  dvne0f1  24609  dvcnvrelem2  24615  dvcnvre  24616  mdeglt  24659  mdegxrcl  24661  mdegcl  24663  ig1peu  24765  ulmss  24985  reeff1o  25035  efifo  25131  dvlog  25234  efopn  25241  lgamcvg2  25632  dchrisum0fno1  26087  usgredgss  26944  hhssims  29051  shsss  29090  pjrni  29479  imaelshi  29835  foresf1o  30265  fnpreimac  30416  tocyc01  30760  cycpmrn  30785  cycpmconjslem2  30797  cyc3conja  30799  dimkerim  31023  smatrcl  31061  locfinreflem  31104  esumcvg  31345  omssubadd  31558  sitgclbn  31601  eulerpartgbij  31630  eulerpartlemgvv  31634  eulerpartlemgf  31637  ballotlemsima  31773  hashf1dmcdm  32356  lfuhgr  32364  mrsubf  32764  msubf  32779  mstapst  32794  mclsind  32817  mclsppslem  32830  orderseqlem  33094  norn  33158  icoreunrn  34643  pibt2  34701  ptrecube  34907  poimirlem1  34908  poimirlem3  34910  poimirlem12  34919  poimirlem16  34923  poimirlem32  34939  broucube  34941  heicant  34942  opnmbllem0  34943  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  volsupnfl  34952  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  indexdom  35024  sstotbnd  35068  prdsbnd  35086  heibor1lem  35102  heiborlem1  35104  rrnval  35120  reheibor  35132  lsatset  36141  elrfirn  39312  isnacs2  39323  nacsfix  39329  coeq0i  39370  diophrw  39376  dnwech  39668  pwssplit4  39709  hbt  39750  rnmptssf  41539  liminfval2  42069  fourierdlem12  42424  fourierdlem42  42454  fourierdlem54  42465  fourierdlem76  42487  fourierdlem85  42496  fourierdlem88  42499  fourierdlem93  42504  fourierdlem113  42524  hoicvr  42850  vonvolmbl2  42965  vonvol2  42966  fafvelrn  43389  fafv2elrn  43453  mgmplusfreseq  44060  elbigolo1  44637  aacllem  44922