Theorem frn 6616

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

Syntax hints:   → wi 4   ⊆ wss 3888  ran crn 5591   Fn wfn 6432  ⟶wf 6433

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 6441

This theorem is referenced by:  frnd  6617  fimass  6630  fimacnv  6631  fco2  6636  fssxp  6637  fimacnvdisj  6661  f00  6665  f0rn0  6668  f1resf1  6688  foconst  6712  ffvelrn  6968  f1ompt  6994  fnfvrnss  7003  rnmptss  7005  isofr2  7224  fiun  7794  fo1stres  7866  fo2ndres  7867  1stcof  7870  2ndcof  7871  fnwelem  7981  tposf2  8075  seqomlem2  8291  oacomf1olem  8404  map0b  8680  mapsnd  8683  fipreima  9134  indexfi  9136  dffi3  9199  oismo  9308  djuin  9685  updjudhcoinlf  9699  updjudhcoinrg  9700  acndom  9816  acndom2  9819  dfac12lem2  9909  dfac12lem3  9910  ackbij1  10003  cfflb  10024  fin23lem40  10116  fin23lem41  10117  isf34lem7  10144  fin1a2lem6  10170  fin1a2lem7  10171  hsmexlem4  10194  hsmexlem5  10195  axdc2lem  10213  axdc3lem2  10216  ttukeylem6  10279  unirnfdomd  10332  pwcfsdom  10348  smobeth  10351  pwfseqlem5  10428  tskurn  10554  wfgru  10581  rpnnen1lem4  12729  rpnnen1lem5  12730  unirnioo  13190  fseqsupcl  13706  fseqsupubi  13707  limsupcl  15191  limsuple  15196  limsupval2  15198  prmreclem6  16631  0ram2  16731  0ramcl  16733  imasdsval2  17236  mrcssv  17332  isacs1i  17375  acsmapd  18281  acsmap2d  18282  gsumval1  18376  dfod2  19180  odcl2  19181  sylow1lem2  19213  efgsfo  19354  gexex  19463  iscyggen2  19490  iscyg3  19495  gsumval3lem1  19515  gsumval3  19517  dprdf1  19645  subgdmdprd  19646  subgdprd  19647  lindfmm  21043  m2cpmmhm  21903  leordtval2  22372  lecldbas  22379  discmp  22558  cmpsub  22560  tgcmp  22561  hauscmplem  22566  2ndcctbss  22615  2ndcsep  22619  comppfsc  22692  kgentop  22702  1stckgen  22714  kgencn2  22717  txuni2  22725  xkoopn  22749  xkouni  22759  xkoccn  22779  ptcnplem  22781  txkgen  22812  xkoco1cn  22817  xkoco2cn  22818  xkococnlem  22819  xkococn  22820  xkoinjcn  22847  hmphdis  22956  zfbas  23056  uzrest  23057  elfm  23107  alexsubALT  23211  efmndtmd  23261  submtmd  23264  symgtgp  23266  tsmsxplem1  23313  blin2  23591  imasf1oxms  23654  tgqioo  23972  xrtgioo  23978  metdscn2  24029  iimulcn  24110  icchmeo  24113  xrhmeo  24118  cnheiborlem  24126  tcphex  24390  tchnmfval  24401  fmcfil  24445  causs  24471  ovolficcss  24642  elovolm  24648  ovoliunlem2  24676  volsup  24729  uniioovol  24752  dyadmbllem  24772  dyadmbl  24773  opnmbllem  24774  opnmblALT  24776  volsup2  24778  mbfconstlem  24800  i1fd  24854  i1f1  24863  itg11  24864  itg1addlem4  24872  itg1addlem4OLD  24873  itg1climres  24888  itg2gt0  24934  limciun  25067  c1liplem1  25169  dvne0f1  25185  dvcnvrelem2  25191  dvcnvre  25192  mdeglt  25239  mdegxrcl  25241  mdegcl  25243  ig1peu  25345  ulmss  25565  reeff1o  25615  efifo  25712  dvlog  25815  efopn  25822  lgamcvg2  26213  dchrisum0fno1  26668  usgredgss  27538  hhssims  29645  shsss  29684  pjrni  30073  imaelshi  30429  foresf1o  30859  fnpreimac  31017  tocyc01  31394  cycpmrn  31419  cycpmconjslem2  31431  cyc3conja  31433  dimkerim  31717  smatrcl  31755  locfinreflem  31799  esumcvg  32063  omssubadd  32276  sitgclbn  32319  eulerpartgbij  32348  eulerpartlemgvv  32352  eulerpartlemgf  32355  ballotlemsima  32491  hashf1dmcdm  33085  lfuhgr  33088  mrsubf  33488  msubf  33503  mstapst  33518  mclsind  33541  mclsppslem  33554  orderseqlem  33810  norn  33863  oldf  34050  icoreunrn  35539  pibt2  35597  ptrecube  35786  poimirlem1  35787  poimirlem3  35789  poimirlem12  35798  poimirlem16  35802  poimirlem32  35818  broucube  35820  heicant  35821  opnmbllem0  35822  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  volsupnfl  35831  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  indexdom  35901  sstotbnd  35942  prdsbnd  35960  heibor1lem  35976  heiborlem1  35978  rrnval  35994  reheibor  36006  lsatset  37011  elrfirn  40524  isnacs2  40535  nacsfix  40541  coeq0i  40582  diophrw  40588  dnwech  40880  pwssplit4  40921  hbt  40962  rnmptssf  42800  liminfval2  43316  fourierdlem12  43667  fourierdlem42  43697  fourierdlem54  43708  fourierdlem76  43730  fourierdlem85  43739  fourierdlem88  43742  fourierdlem93  43747  fourierdlem113  43767  hoicvr  44093  vonvolmbl2  44208  vonvol2  44209  fafvelrn  44673  fafv2elrn  44737  mgmplusfreseq  45338  elbigolo1  45914  aacllem  46516