Theorem frn 6754

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

Syntax hints:   → wi 4   ⊆ wss 3976  ran crn 5701   Fn wfn 6568  ⟶wf 6569

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 6577

This theorem is referenced by:  frnd  6755  fimass  6767  fimacnv  6769  fco2  6774  fssxp  6775  fimacnvdisj  6799  f00  6803  f0rn0  6806  f1resf1  6825  foconst  6849  ffvelcdm  7115  f1ompt  7145  fnfvrnss  7155  rnmptss  7157  isofr2  7380  fiun  7983  fo1stres  8056  fo2ndres  8057  1stcof  8060  2ndcof  8061  fnwelem  8172  orderseqlem  8198  tposf2  8291  seqomlem2  8507  oacomf1olem  8620  naddunif  8749  naddasslem1  8750  naddasslem2  8751  map0b  8941  mapsnd  8944  fipreima  9428  indexfi  9430  dffi3  9500  oismo  9609  djuin  9987  updjudhcoinlf  10001  updjudhcoinrg  10002  acndom  10120  acndom2  10123  dfac12lem2  10214  dfac12lem3  10215  ackbij1  10306  cfflb  10328  fin23lem40  10420  fin23lem41  10421  isf34lem7  10448  fin1a2lem6  10474  fin1a2lem7  10475  hsmexlem4  10498  hsmexlem5  10499  axdc2lem  10517  axdc3lem2  10520  ttukeylem6  10583  unirnfdomd  10636  pwcfsdom  10652  smobeth  10655  pwfseqlem5  10732  tskurn  10858  wfgru  10885  rpnnen1lem4  13045  rpnnen1lem5  13046  unirnioo  13509  fseqsupcl  14028  fseqsupubi  14029  hashf1dmcdm  14493  limsupcl  15519  limsuple  15524  limsupval2  15526  prmreclem6  16968  0ram2  17068  0ramcl  17070  imasdsval2  17576  mrcssv  17672  isacs1i  17715  acsmapd  18624  acsmap2d  18625  gsumval1  18721  dfod2  19606  odcl2  19607  sylow1lem2  19641  efgsfo  19781  gexex  19895  iscyggen2  19923  iscyg3  19928  gsumval3lem1  19947  gsumval3  19949  dprdf1  20077  subgdmdprd  20078  subgdprd  20079  lindfmm  21870  m2cpmmhm  22772  leordtval2  23241  lecldbas  23248  discmp  23427  cmpsub  23429  tgcmp  23430  hauscmplem  23435  2ndcctbss  23484  2ndcsep  23488  comppfsc  23561  kgentop  23571  1stckgen  23583  kgencn2  23586  txuni2  23594  xkoopn  23618  xkouni  23628  xkoccn  23648  ptcnplem  23650  txkgen  23681  xkoco1cn  23686  xkoco2cn  23687  xkococnlem  23688  xkococn  23689  xkoinjcn  23716  hmphdis  23825  zfbas  23925  uzrest  23926  elfm  23976  alexsubALT  24080  efmndtmd  24130  submtmd  24133  symgtgp  24135  tsmsxplem1  24182  blin2  24460  imasf1oxms  24523  tgqioo  24841  xrtgioo  24847  metdscn2  24898  iimulcn  24986  iimulcnOLD  24987  icchmeo  24990  icchmeoOLD  24991  xrhmeo  24996  cnheiborlem  25005  tcphex  25270  tchnmfval  25281  fmcfil  25325  causs  25351  ovolficcss  25523  elovolm  25529  ovoliunlem2  25557  volsup  25610  uniioovol  25633  dyadmbllem  25653  dyadmbl  25654  opnmbllem  25655  opnmblALT  25657  volsup2  25659  mbfconstlem  25681  i1fd  25735  i1f1  25744  itg11  25745  itg1addlem4  25753  itg1addlem4OLD  25754  itg1climres  25769  itg2gt0  25815  limciun  25949  c1liplem1  26055  dvne0f1  26071  dvcnvrelem2  26077  dvcnvre  26078  mdeglt  26124  mdegxrcl  26126  mdegcl  26128  ig1peu  26234  ulmss  26458  reeff1o  26509  efifo  26607  dvlog  26711  efopn  26718  lgamcvg2  27116  dchrisum0fno1  27573  norn  27714  oldf  27914  usgredgss  29194  hhssims  31306  shsss  31345  pjrni  31734  imaelshi  32090  foresf1o  32532  fnpreimac  32689  tocyc01  33111  cycpmrn  33136  cycpmconjslem2  33148  cyc3conja  33150  dimkerim  33640  smatrcl  33742  locfinreflem  33786  esumcvg  34050  omssubadd  34265  sitgclbn  34308  eulerpartgbij  34337  eulerpartlemgvv  34341  eulerpartlemgf  34344  ballotlemsima  34480  lfuhgr  35085  mrsubf  35485  msubf  35500  mstapst  35515  mclsind  35538  mclsppslem  35551  icoreunrn  37325  pibt2  37383  ptrecube  37580  poimirlem1  37581  poimirlem3  37583  poimirlem12  37592  poimirlem16  37596  poimirlem32  37612  broucube  37614  heicant  37615  opnmbllem0  37616  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  volsupnfl  37625  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  indexdom  37694  sstotbnd  37735  prdsbnd  37753  heibor1lem  37769  heiborlem1  37771  rrnval  37787  reheibor  37799  lsatset  38946  aks6d1c2  42087  aks6d1c6lem3  42129  aks6d1c6isolem1  42131  aks6d1c7lem1  42137  unitscyglem1  42152  elrfirn  42651  isnacs2  42662  nacsfix  42668  coeq0i  42709  diophrw  42715  dnwech  43005  pwssplit4  43046  hbt  43087  rnmptssf  45156  rnmptssff  45184  liminfval2  45689  fourierdlem12  46040  fourierdlem42  46070  fourierdlem54  46081  fourierdlem76  46103  fourierdlem85  46112  fourierdlem88  46115  fourierdlem93  46120  fourierdlem113  46140  hoicvr  46469  vonvolmbl2  46584  vonvol2  46585  fafvelcdm  47085  fafv2elcdm  47149  mgmplusfreseq  47888  elbigolo1  48291  aacllem  48895