Theorem frn 6713

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3905  ran crn 5662   Fn wfn 6531  ⟶wf 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-f 6540

This theorem is used by:  frnd  6714  fimass  6726  fimacnv  6728  fco2  6732  fssxp  6733  fimacnvdisj  6756  f00  6760  f0rn0  6763  f1resf1  6784  foconst  6807  ffvelcdm  7076  f1ompt  7106  fnfvrnss  7116  rnmptss  7118  isofr2  7342  fiun  7936  fo1stres  8008  fo2ndres  8009  1stcof  8012  2ndcof  8013  fnwelem  8123  orderseqlem  8149  tposf2  8242  seqomlem2  8434  oacomf1olem  8545  naddunif  8676  naddasslem1  8677  naddasslem2  8678  map0b  8877  mapsnd  8880  fipreima  9311  indexfi  9313  dffi3  9387  oismo  9498  djuin  9909  updjudhcoinlf  9923  updjudhcoinrg  9924  acndom  10040  acndom2  10043  dfac12lem2  10133  dfac12lem3  10134  ackbij1  10225  cfflb  10247  fin23lem40  10339  fin23lem41  10340  isf34lem7  10367  fin1a2lem6  10393  fin1a2lem7  10394  hsmexlem4  10417  hsmexlem5  10418  axdc2lem  10436  axdc3lem2  10439  ttukeylem6  10502  unirnfdomd  10556  pwcfsdom  10572  smobeth  10575  pwfseqlem5  10652  tskurn  10778  wfgru  10805  rpnnen1lem4  13008  rpnnen1lem5  13009  unirnioo  13480  fseqsupcl  14018  fseqsupubi  14019  hashf1dmcdm  14486  limsupcl  15529  limsuple  15534  limsupval2  15536  prmreclem6  16985  0ram2  17085  0ramcl  17087  imasdsval2  17574  mrcssv  17674  isacs1i  17717  acsmapd  18614  acsmap2d  18615  gsumval1  18745  dfod2  19638  odcl2  19639  sylow1lem2  19673  efgsfo  19813  gexex  19927  iscyggen2  19955  iscyg3  19960  gsumval3lem1  19979  gsumval3  19981  dprdf1  20109  subgdmdprd  20110  subgdprd  20111  lindfmm  21986  m2cpmmhm  22911  leordtval2  23378  lecldbas  23385  discmp  23564  cmpsub  23566  tgcmp  23567  hauscmplem  23572  2ndcctbss  23621  2ndcsep  23625  comppfsc  23698  kgentop  23708  1stckgen  23720  kgencn2  23723  txuni2  23731  xkoopn  23755  xkouni  23765  xkoccn  23785  ptcnplem  23787  txkgen  23818  xkoco1cn  23823  xkoco2cn  23824  xkococnlem  23825  xkococn  23826  xkoinjcn  23853  hmphdis  23962  zfbas  24062  uzrest  24063  elfm  24113  alexsubALT  24217  efmndtmd  24267  submtmd  24270  symgtgp  24272  tsmsxplem1  24319  blin2  24595  imasf1oxms  24655  tgqioo  24966  xrtgioo  24973  metdscn2  25024  iimulcn  25106  icchmeo  25109  xrhmeo  25114  cnheiborlem  25122  tcphex  25385  tchnmfval  25396  fmcfil  25440  causs  25466  ovolficcss  25637  elovolm  25643  ovoliunlem2  25671  volsup  25724  uniioovol  25747  dyadmbllem  25767  dyadmbl  25768  opnmbllem  25769  opnmblALT  25771  volsup2  25773  mbfconstlem  25795  i1fd  25849  i1f1  25858  itg11  25859  itg1addlem4  25867  itg1climres  25882  itg2gt0  25928  limciun  26062  c1liplem1  26164  dvne0f1  26180  dvcnvrelem2  26186  dvcnvre  26187  mdeglt  26231  mdegxrcl  26233  mdegcl  26235  ig1peu  26341  ulmss  26569  reeff1o  26619  efifo  26721  dvlog  26825  efopn  26832  lgamcvg2  27228  dchrisum0fno1  27684  norn  27824  oldf  28039  usgredgss  29518  hhssims  31635  shsss  31674  pjrni  32063  imaelshi  32419  foresf1o  32859  fnpreimac  33024  tocyc01  33447  cycpmrn  33472  cycpmconjslem2  33484  cyc3conja  33486  dimkerim  34026  smatrcl  34195  locfinreflem  34239  esumcvg  34485  omssubadd  34699  sitgclbn  34742  eulerpartgbij  34771  eulerpartlemgvv  34775  eulerpartlemgf  34778  ballotlemsima  34915  lfuhgr  35618  mrsubf  36017  msubf  36032  mstapst  36047  mclsind  36070  mclsppslem  36083  icoreunrn  38033  pibt2  38091  ptrecube  38299  poimirlem1  38300  poimirlem3  38302  poimirlem12  38311  poimirlem16  38315  poimirlem32  38331  broucube  38333  heicant  38334  opnmbllem0  38335  mblfinlem1  38336  mblfinlem2  38337  mblfinlem3  38338  mblfinlem4  38339  ismblfin  38340  volsupnfl  38344  ftc1anclem5  38376  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  indexdom  38413  sstotbnd  38454  prdsbnd  38472  heibor1lem  38488  heiborlem1  38490  rrnval  38506  reheibor  38518  lsatset  39792  aks6d1c2  42925  aks6d1c6lem3  42967  aks6d1c6isolem1  42969  aks6d1c7lem1  42975  unitscyglem1  42990  elrfirn  43454  isnacs2  43465  nacsfix  43471  coeq0i  43512  diophrw  43518  dnwech  43803  pwssplit4  43844  hbt  43885  rnmptssf  45990  rnmptssff  46017  liminfval2  46510  fourierdlem12  46861  fourierdlem42  46891  fourierdlem54  46902  fourierdlem76  46924  fourierdlem85  46933  fourierdlem88  46936  fourierdlem93  46941  hoicvr  47290  vonvolmbl2  47405  vonvol2  47406  fafvelcdm  47935  fafv2elcdm  47999  mgmplusfreseq  48958  elbigolo1  49365  aacllem  50649