Theorem frn 6712

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

Syntax hints:   → wi 4   ⊆ wss 3926  ran crn 5655   Fn wfn 6525  ⟶wf 6526

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 6534

This theorem is referenced by:  frnd  6713  fimass  6725  fimacnv  6727  fco2  6731  fssxp  6732  fimacnvdisj  6755  f00  6759  f0rn0  6762  f1resf1  6781  foconst  6804  ffvelcdm  7070  f1ompt  7100  fnfvrnss  7110  rnmptss  7112  isofr2  7336  fiun  7939  fo1stres  8012  fo2ndres  8013  1stcof  8016  2ndcof  8017  fnwelem  8128  orderseqlem  8154  tposf2  8247  seqomlem2  8463  oacomf1olem  8574  naddunif  8703  naddasslem1  8704  naddasslem2  8705  map0b  8895  mapsnd  8898  fipreima  9368  indexfi  9370  dffi3  9441  oismo  9552  djuin  9930  updjudhcoinlf  9944  updjudhcoinrg  9945  acndom  10063  acndom2  10066  dfac12lem2  10157  dfac12lem3  10158  ackbij1  10249  cfflb  10271  fin23lem40  10363  fin23lem41  10364  isf34lem7  10391  fin1a2lem6  10417  fin1a2lem7  10418  hsmexlem4  10441  hsmexlem5  10442  axdc2lem  10460  axdc3lem2  10463  ttukeylem6  10526  unirnfdomd  10579  pwcfsdom  10595  smobeth  10598  pwfseqlem5  10675  tskurn  10801  wfgru  10828  rpnnen1lem4  12994  rpnnen1lem5  12995  unirnioo  13464  fseqsupcl  13993  fseqsupubi  13994  hashf1dmcdm  14460  limsupcl  15487  limsuple  15492  limsupval2  15494  prmreclem6  16939  0ram2  17039  0ramcl  17041  imasdsval2  17528  mrcssv  17624  isacs1i  17667  acsmapd  18562  acsmap2d  18563  gsumval1  18659  dfod2  19543  odcl2  19544  sylow1lem2  19578  efgsfo  19718  gexex  19832  iscyggen2  19860  iscyg3  19865  gsumval3lem1  19884  gsumval3  19886  dprdf1  20014  subgdmdprd  20015  subgdprd  20016  lindfmm  21785  m2cpmmhm  22681  leordtval2  23148  lecldbas  23155  discmp  23334  cmpsub  23336  tgcmp  23337  hauscmplem  23342  2ndcctbss  23391  2ndcsep  23395  comppfsc  23468  kgentop  23478  1stckgen  23490  kgencn2  23493  txuni2  23501  xkoopn  23525  xkouni  23535  xkoccn  23555  ptcnplem  23557  txkgen  23588  xkoco1cn  23593  xkoco2cn  23594  xkococnlem  23595  xkococn  23596  xkoinjcn  23623  hmphdis  23732  zfbas  23832  uzrest  23833  elfm  23883  alexsubALT  23987  efmndtmd  24037  submtmd  24040  symgtgp  24042  tsmsxplem1  24089  blin2  24366  imasf1oxms  24426  tgqioo  24737  xrtgioo  24744  metdscn2  24795  iimulcn  24883  iimulcnOLD  24884  icchmeo  24887  icchmeoOLD  24888  xrhmeo  24893  cnheiborlem  24902  tcphex  25167  tchnmfval  25178  fmcfil  25222  causs  25248  ovolficcss  25420  elovolm  25426  ovoliunlem2  25454  volsup  25507  uniioovol  25530  dyadmbllem  25550  dyadmbl  25551  opnmbllem  25552  opnmblALT  25554  volsup2  25556  mbfconstlem  25578  i1fd  25632  i1f1  25641  itg11  25642  itg1addlem4  25650  itg1climres  25665  itg2gt0  25711  limciun  25845  c1liplem1  25951  dvne0f1  25967  dvcnvrelem2  25973  dvcnvre  25974  mdeglt  26020  mdegxrcl  26022  mdegcl  26024  ig1peu  26130  ulmss  26356  reeff1o  26407  efifo  26506  dvlog  26610  efopn  26617  lgamcvg2  27015  dchrisum0fno1  27472  norn  27613  oldf  27813  usgredgss  29084  hhssims  31201  shsss  31240  pjrni  31629  imaelshi  31985  foresf1o  32431  fnpreimac  32595  tocyc01  33075  cycpmrn  33100  cycpmconjslem2  33112  cyc3conja  33114  dimkerim  33613  smatrcl  33773  locfinreflem  33817  esumcvg  34063  omssubadd  34278  sitgclbn  34321  eulerpartgbij  34350  eulerpartlemgvv  34354  eulerpartlemgf  34357  ballotlemsima  34494  lfuhgr  35086  mrsubf  35485  msubf  35500  mstapst  35515  mclsind  35538  mclsppslem  35551  icoreunrn  37323  pibt2  37381  ptrecube  37590  poimirlem1  37591  poimirlem3  37593  poimirlem12  37602  poimirlem16  37606  poimirlem32  37622  broucube  37624  heicant  37625  opnmbllem0  37626  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  volsupnfl  37635  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  indexdom  37704  sstotbnd  37745  prdsbnd  37763  heibor1lem  37779  heiborlem1  37781  rrnval  37797  reheibor  37809  lsatset  38954  aks6d1c2  42089  aks6d1c6lem3  42131  aks6d1c6isolem1  42133  aks6d1c7lem1  42139  unitscyglem1  42154  elrfirn  42665  isnacs2  42676  nacsfix  42682  coeq0i  42723  diophrw  42729  dnwech  43019  pwssplit4  43060  hbt  43101  rnmptssf  45219  rnmptssff  45246  liminfval2  45745  fourierdlem12  46096  fourierdlem42  46126  fourierdlem54  46137  fourierdlem76  46159  fourierdlem85  46168  fourierdlem88  46171  fourierdlem93  46176  fourierdlem113  46196  hoicvr  46525  vonvolmbl2  46640  vonvol2  46641  fafvelcdm  47147  fafv2elcdm  47211  mgmplusfreseq  48088  elbigolo1  48485  aacllem  49613