Theorem frn 6591

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

Syntax hints:   → wi 4   ⊆ wss 3883  ran crn 5581   Fn wfn 6413  ⟶wf 6414

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 396  df-f 6422

This theorem is referenced by:  frnd  6592  fimass  6605  fimacnv  6606  fco2  6611  fssxp  6612  fimacnvdisj  6636  f00  6640  f0rn0  6643  f1resf1  6663  foconst  6687  ffvelrn  6941  f1ompt  6967  fnfvrnss  6976  rnmptss  6978  isofr2  7195  fiun  7759  fo1stres  7830  fo2ndres  7831  1stcof  7834  2ndcof  7835  fnwelem  7943  tposf2  8037  seqomlem2  8252  oacomf1olem  8357  map0b  8629  mapsnd  8632  fipreima  9055  indexfi  9057  dffi3  9120  oismo  9229  djuin  9607  updjudhcoinlf  9621  updjudhcoinrg  9622  acndom  9738  acndom2  9741  dfac12lem2  9831  dfac12lem3  9832  ackbij1  9925  cfflb  9946  fin23lem40  10038  fin23lem41  10039  isf34lem7  10066  fin1a2lem6  10092  fin1a2lem7  10093  hsmexlem4  10116  hsmexlem5  10117  axdc2lem  10135  axdc3lem2  10138  ttukeylem6  10201  unirnfdomd  10254  pwcfsdom  10270  smobeth  10273  pwfseqlem5  10350  tskurn  10476  wfgru  10503  rpnnen1lem4  12649  rpnnen1lem5  12650  unirnioo  13110  fseqsupcl  13625  fseqsupubi  13626  limsupcl  15110  limsuple  15115  limsupval2  15117  prmreclem6  16550  0ram2  16650  0ramcl  16652  imasdsval2  17144  mrcssv  17240  isacs1i  17283  acsmapd  18187  acsmap2d  18188  gsumval1  18282  dfod2  19086  odcl2  19087  sylow1lem2  19119  efgsfo  19260  gexex  19369  iscyggen2  19396  iscyg3  19401  gsumval3lem1  19421  gsumval3  19423  dprdf1  19551  subgdmdprd  19552  subgdprd  19553  lindfmm  20944  m2cpmmhm  21802  leordtval2  22271  lecldbas  22278  discmp  22457  cmpsub  22459  tgcmp  22460  hauscmplem  22465  2ndcctbss  22514  2ndcsep  22518  comppfsc  22591  kgentop  22601  1stckgen  22613  kgencn2  22616  txuni2  22624  xkoopn  22648  xkouni  22658  xkoccn  22678  ptcnplem  22680  txkgen  22711  xkoco1cn  22716  xkoco2cn  22717  xkococnlem  22718  xkococn  22719  xkoinjcn  22746  hmphdis  22855  zfbas  22955  uzrest  22956  elfm  23006  alexsubALT  23110  efmndtmd  23160  submtmd  23163  symgtgp  23165  tsmsxplem1  23212  blin2  23490  imasf1oxms  23551  tgqioo  23869  xrtgioo  23875  metdscn2  23926  iimulcn  24007  icchmeo  24010  xrhmeo  24015  cnheiborlem  24023  tcphex  24286  tchnmfval  24297  fmcfil  24341  causs  24367  ovolficcss  24538  elovolm  24544  ovoliunlem2  24572  volsup  24625  uniioovol  24648  dyadmbllem  24668  dyadmbl  24669  opnmbllem  24670  opnmblALT  24672  volsup2  24674  mbfconstlem  24696  i1fd  24750  i1f1  24759  itg11  24760  itg1addlem4  24768  itg1addlem4OLD  24769  itg1climres  24784  itg2gt0  24830  limciun  24963  c1liplem1  25065  dvne0f1  25081  dvcnvrelem2  25087  dvcnvre  25088  mdeglt  25135  mdegxrcl  25137  mdegcl  25139  ig1peu  25241  ulmss  25461  reeff1o  25511  efifo  25608  dvlog  25711  efopn  25718  lgamcvg2  26109  dchrisum0fno1  26564  usgredgss  27432  hhssims  29537  shsss  29576  pjrni  29965  imaelshi  30321  foresf1o  30751  fnpreimac  30910  tocyc01  31287  cycpmrn  31312  cycpmconjslem2  31324  cyc3conja  31326  dimkerim  31610  smatrcl  31648  locfinreflem  31692  esumcvg  31954  omssubadd  32167  sitgclbn  32210  eulerpartgbij  32239  eulerpartlemgvv  32243  eulerpartlemgf  32246  ballotlemsima  32382  hashf1dmcdm  32976  lfuhgr  32979  mrsubf  33379  msubf  33394  mstapst  33409  mclsind  33432  mclsppslem  33445  orderseqlem  33728  norn  33781  oldf  33968  icoreunrn  35457  pibt2  35515  ptrecube  35704  poimirlem1  35705  poimirlem3  35707  poimirlem12  35716  poimirlem16  35720  poimirlem32  35736  broucube  35738  heicant  35739  opnmbllem0  35740  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  volsupnfl  35749  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  indexdom  35819  sstotbnd  35860  prdsbnd  35878  heibor1lem  35894  heiborlem1  35896  rrnval  35912  reheibor  35924  lsatset  36931  elrfirn  40433  isnacs2  40444  nacsfix  40450  coeq0i  40491  diophrw  40497  dnwech  40789  pwssplit4  40830  hbt  40871  rnmptssf  42682  liminfval2  43199  fourierdlem12  43550  fourierdlem42  43580  fourierdlem54  43591  fourierdlem76  43613  fourierdlem85  43622  fourierdlem88  43625  fourierdlem93  43630  fourierdlem113  43650  hoicvr  43976  vonvolmbl2  44091  vonvol2  44092  fafvelrn  44549  fafv2elrn  44613  mgmplusfreseq  45215  elbigolo1  45791  aacllem  46391