Theorem frn 6679

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

Syntax hints:   → wi 4   ⊆ wss 3903  ran crn 5635   Fn wfn 6497  ⟶wf 6498

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 6506

This theorem is referenced by:  frnd  6680  fimass  6692  fimacnv  6694  fco2  6698  fssxp  6699  fimacnvdisj  6722  f00  6726  f0rn0  6729  f1resf1  6748  foconst  6771  ffvelcdm  7037  f1ompt  7067  fnfvrnss  7077  rnmptss  7079  isofr2  7302  fiun  7899  fo1stres  7971  fo2ndres  7972  1stcof  7975  2ndcof  7976  fnwelem  8085  orderseqlem  8111  tposf2  8204  seqomlem2  8394  oacomf1olem  8503  naddunif  8633  naddasslem1  8634  naddasslem2  8635  map0b  8835  mapsnd  8838  fipreima  9272  indexfi  9274  dffi3  9348  oismo  9459  djuin  9844  updjudhcoinlf  9858  updjudhcoinrg  9859  acndom  9975  acndom2  9978  dfac12lem2  10069  dfac12lem3  10070  ackbij1  10161  cfflb  10183  fin23lem40  10275  fin23lem41  10276  isf34lem7  10303  fin1a2lem6  10329  fin1a2lem7  10330  hsmexlem4  10353  hsmexlem5  10354  axdc2lem  10372  axdc3lem2  10375  ttukeylem6  10438  unirnfdomd  10492  pwcfsdom  10508  smobeth  10511  pwfseqlem5  10588  tskurn  10714  wfgru  10741  rpnnen1lem4  12907  rpnnen1lem5  12908  unirnioo  13379  fseqsupcl  13914  fseqsupubi  13915  hashf1dmcdm  14381  limsupcl  15410  limsuple  15415  limsupval2  15417  prmreclem6  16863  0ram2  16963  0ramcl  16965  imasdsval2  17451  mrcssv  17551  isacs1i  17594  acsmapd  18491  acsmap2d  18492  gsumval1  18622  dfod2  19510  odcl2  19511  sylow1lem2  19545  efgsfo  19685  gexex  19799  iscyggen2  19827  iscyg3  19832  gsumval3lem1  19851  gsumval3  19853  dprdf1  19981  subgdmdprd  19982  subgdprd  19983  lindfmm  21799  m2cpmmhm  22706  leordtval2  23173  lecldbas  23180  discmp  23359  cmpsub  23361  tgcmp  23362  hauscmplem  23367  2ndcctbss  23416  2ndcsep  23420  comppfsc  23493  kgentop  23503  1stckgen  23515  kgencn2  23518  txuni2  23526  xkoopn  23550  xkouni  23560  xkoccn  23580  ptcnplem  23582  txkgen  23613  xkoco1cn  23618  xkoco2cn  23619  xkococnlem  23620  xkococn  23621  xkoinjcn  23648  hmphdis  23757  zfbas  23857  uzrest  23858  elfm  23908  alexsubALT  24012  efmndtmd  24062  submtmd  24065  symgtgp  24067  tsmsxplem1  24114  blin2  24390  imasf1oxms  24450  tgqioo  24761  xrtgioo  24768  metdscn2  24819  iimulcn  24907  iimulcnOLD  24908  icchmeo  24911  icchmeoOLD  24912  xrhmeo  24917  cnheiborlem  24926  tcphex  25190  tchnmfval  25201  fmcfil  25245  causs  25271  ovolficcss  25443  elovolm  25449  ovoliunlem2  25477  volsup  25530  uniioovol  25553  dyadmbllem  25573  dyadmbl  25574  opnmbllem  25575  opnmblALT  25577  volsup2  25579  mbfconstlem  25601  i1fd  25655  i1f1  25664  itg11  25665  itg1addlem4  25673  itg1climres  25688  itg2gt0  25734  limciun  25868  c1liplem1  25974  dvne0f1  25990  dvcnvrelem2  25996  dvcnvre  25997  mdeglt  26043  mdegxrcl  26045  mdegcl  26047  ig1peu  26153  ulmss  26379  reeff1o  26430  efifo  26529  dvlog  26633  efopn  26640  lgamcvg2  27038  dchrisum0fno1  27495  norn  27636  oldf  27850  usgredgss  29250  hhssims  31368  shsss  31407  pjrni  31796  imaelshi  32152  foresf1o  32597  fnpreimac  32766  tocyc01  33218  cycpmrn  33243  cycpmconjslem2  33255  cyc3conja  33257  dimkerim  33811  smatrcl  33980  locfinreflem  34024  esumcvg  34270  omssubadd  34484  sitgclbn  34527  eulerpartgbij  34556  eulerpartlemgvv  34560  eulerpartlemgf  34563  ballotlemsima  34700  lfuhgr  35340  mrsubf  35739  msubf  35754  mstapst  35769  mclsind  35792  mclsppslem  35805  icoreunrn  37641  pibt2  37699  ptrecube  37900  poimirlem1  37901  poimirlem3  37903  poimirlem12  37912  poimirlem16  37916  poimirlem32  37932  broucube  37934  heicant  37935  opnmbllem0  37936  mblfinlem1  37937  mblfinlem2  37938  mblfinlem3  37939  mblfinlem4  37940  ismblfin  37941  volsupnfl  37945  ftc1anclem5  37977  ftc1anclem7  37979  ftc1anclem8  37980  ftc1anc  37981  indexdom  38014  sstotbnd  38055  prdsbnd  38073  heibor1lem  38089  heiborlem1  38091  rrnval  38107  reheibor  38119  lsatset  39395  aks6d1c2  42529  aks6d1c6lem3  42571  aks6d1c6isolem1  42573  aks6d1c7lem1  42579  unitscyglem1  42594  elrfirn  43081  isnacs2  43092  nacsfix  43098  coeq0i  43139  diophrw  43145  dnwech  43434  pwssplit4  43475  hbt  43516  rnmptssf  45634  rnmptssff  45661  liminfval2  46155  fourierdlem12  46506  fourierdlem42  46536  fourierdlem54  46547  fourierdlem76  46569  fourierdlem85  46578  fourierdlem88  46581  fourierdlem93  46586  fourierdlem113  46606  hoicvr  46935  vonvolmbl2  47050  vonvol2  47051  fafvelcdm  47559  fafv2elcdm  47623  mgmplusfreseq  48554  elbigolo1  48946  aacllem  50189