Theorem frn 6669

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

Syntax hints:   → wi 4   ⊆ wss 3901  ran crn 5625   Fn wfn 6487  ⟶wf 6488

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 6496

This theorem is referenced by:  frnd  6670  fimass  6682  fimacnv  6684  fco2  6688  fssxp  6689  fimacnvdisj  6712  f00  6716  f0rn0  6719  f1resf1  6738  foconst  6761  ffvelcdm  7026  f1ompt  7056  fnfvrnss  7066  rnmptss  7068  isofr2  7290  fiun  7887  fo1stres  7959  fo2ndres  7960  1stcof  7963  2ndcof  7964  fnwelem  8073  orderseqlem  8099  tposf2  8192  seqomlem2  8382  oacomf1olem  8491  naddunif  8621  naddasslem1  8622  naddasslem2  8623  map0b  8821  mapsnd  8824  fipreima  9258  indexfi  9260  dffi3  9334  oismo  9445  djuin  9830  updjudhcoinlf  9844  updjudhcoinrg  9845  acndom  9961  acndom2  9964  dfac12lem2  10055  dfac12lem3  10056  ackbij1  10147  cfflb  10169  fin23lem40  10261  fin23lem41  10262  isf34lem7  10289  fin1a2lem6  10315  fin1a2lem7  10316  hsmexlem4  10339  hsmexlem5  10340  axdc2lem  10358  axdc3lem2  10361  ttukeylem6  10424  unirnfdomd  10478  pwcfsdom  10494  smobeth  10497  pwfseqlem5  10574  tskurn  10700  wfgru  10727  rpnnen1lem4  12893  rpnnen1lem5  12894  unirnioo  13365  fseqsupcl  13900  fseqsupubi  13901  hashf1dmcdm  14367  limsupcl  15396  limsuple  15401  limsupval2  15403  prmreclem6  16849  0ram2  16949  0ramcl  16951  imasdsval2  17437  mrcssv  17537  isacs1i  17580  acsmapd  18477  acsmap2d  18478  gsumval1  18608  dfod2  19493  odcl2  19494  sylow1lem2  19528  efgsfo  19668  gexex  19782  iscyggen2  19810  iscyg3  19815  gsumval3lem1  19834  gsumval3  19836  dprdf1  19964  subgdmdprd  19965  subgdprd  19966  lindfmm  21782  m2cpmmhm  22689  leordtval2  23156  lecldbas  23163  discmp  23342  cmpsub  23344  tgcmp  23345  hauscmplem  23350  2ndcctbss  23399  2ndcsep  23403  comppfsc  23476  kgentop  23486  1stckgen  23498  kgencn2  23501  txuni2  23509  xkoopn  23533  xkouni  23543  xkoccn  23563  ptcnplem  23565  txkgen  23596  xkoco1cn  23601  xkoco2cn  23602  xkococnlem  23603  xkococn  23604  xkoinjcn  23631  hmphdis  23740  zfbas  23840  uzrest  23841  elfm  23891  alexsubALT  23995  efmndtmd  24045  submtmd  24048  symgtgp  24050  tsmsxplem1  24097  blin2  24373  imasf1oxms  24433  tgqioo  24744  xrtgioo  24751  metdscn2  24802  iimulcn  24890  iimulcnOLD  24891  icchmeo  24894  icchmeoOLD  24895  xrhmeo  24900  cnheiborlem  24909  tcphex  25173  tchnmfval  25184  fmcfil  25228  causs  25254  ovolficcss  25426  elovolm  25432  ovoliunlem2  25460  volsup  25513  uniioovol  25536  dyadmbllem  25556  dyadmbl  25557  opnmbllem  25558  opnmblALT  25560  volsup2  25562  mbfconstlem  25584  i1fd  25638  i1f1  25647  itg11  25648  itg1addlem4  25656  itg1climres  25671  itg2gt0  25717  limciun  25851  c1liplem1  25957  dvne0f1  25973  dvcnvrelem2  25979  dvcnvre  25980  mdeglt  26026  mdegxrcl  26028  mdegcl  26030  ig1peu  26136  ulmss  26362  reeff1o  26413  efifo  26512  dvlog  26616  efopn  26623  lgamcvg2  27021  dchrisum0fno1  27478  norn  27619  oldf  27833  usgredgss  29232  hhssims  31349  shsss  31388  pjrni  31777  imaelshi  32133  foresf1o  32579  fnpreimac  32749  tocyc01  33200  cycpmrn  33225  cycpmconjslem2  33237  cyc3conja  33239  dimkerim  33784  smatrcl  33953  locfinreflem  33997  esumcvg  34243  omssubadd  34457  sitgclbn  34500  eulerpartgbij  34529  eulerpartlemgvv  34533  eulerpartlemgf  34536  ballotlemsima  34673  lfuhgr  35312  mrsubf  35711  msubf  35726  mstapst  35741  mclsind  35764  mclsppslem  35777  icoreunrn  37564  pibt2  37622  ptrecube  37821  poimirlem1  37822  poimirlem3  37824  poimirlem12  37833  poimirlem16  37837  poimirlem32  37853  broucube  37855  heicant  37856  opnmbllem0  37857  mblfinlem1  37858  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  volsupnfl  37866  ftc1anclem5  37898  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  indexdom  37935  sstotbnd  37976  prdsbnd  37994  heibor1lem  38010  heiborlem1  38012  rrnval  38028  reheibor  38040  lsatset  39250  aks6d1c2  42384  aks6d1c6lem3  42426  aks6d1c6isolem1  42428  aks6d1c7lem1  42434  unitscyglem1  42449  elrfirn  42937  isnacs2  42948  nacsfix  42954  coeq0i  42995  diophrw  43001  dnwech  43290  pwssplit4  43331  hbt  43372  rnmptssf  45491  rnmptssff  45518  liminfval2  46012  fourierdlem12  46363  fourierdlem42  46393  fourierdlem54  46404  fourierdlem76  46426  fourierdlem85  46435  fourierdlem88  46438  fourierdlem93  46443  fourierdlem113  46463  hoicvr  46792  vonvolmbl2  46907  vonvol2  46908  fafvelcdm  47416  fafv2elcdm  47480  mgmplusfreseq  48411  elbigolo1  48803  aacllem  50046