Theorem frn 6743

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

Syntax hints:   → wi 4   ⊆ wss 3962  ran crn 5689   Fn wfn 6557  ⟶wf 6558

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 6566

This theorem is referenced by:  frnd  6744  fimass  6756  fimacnv  6758  fco2  6762  fssxp  6763  fimacnvdisj  6786  f00  6790  f0rn0  6793  f1resf1  6812  foconst  6835  ffvelcdm  7100  f1ompt  7130  fnfvrnss  7140  rnmptss  7142  isofr2  7363  fiun  7965  fo1stres  8038  fo2ndres  8039  1stcof  8042  2ndcof  8043  fnwelem  8154  orderseqlem  8180  tposf2  8273  seqomlem2  8489  oacomf1olem  8600  naddunif  8729  naddasslem1  8730  naddasslem2  8731  map0b  8921  mapsnd  8924  fipreima  9395  indexfi  9397  dffi3  9468  oismo  9577  djuin  9955  updjudhcoinlf  9969  updjudhcoinrg  9970  acndom  10088  acndom2  10091  dfac12lem2  10182  dfac12lem3  10183  ackbij1  10274  cfflb  10296  fin23lem40  10388  fin23lem41  10389  isf34lem7  10416  fin1a2lem6  10442  fin1a2lem7  10443  hsmexlem4  10466  hsmexlem5  10467  axdc2lem  10485  axdc3lem2  10488  ttukeylem6  10551  unirnfdomd  10604  pwcfsdom  10620  smobeth  10623  pwfseqlem5  10700  tskurn  10826  wfgru  10853  rpnnen1lem4  13019  rpnnen1lem5  13020  unirnioo  13485  fseqsupcl  14014  fseqsupubi  14015  hashf1dmcdm  14479  limsupcl  15505  limsuple  15510  limsupval2  15512  prmreclem6  16954  0ram2  17054  0ramcl  17056  imasdsval2  17562  mrcssv  17658  isacs1i  17701  acsmapd  18611  acsmap2d  18612  gsumval1  18708  dfod2  19596  odcl2  19597  sylow1lem2  19631  efgsfo  19771  gexex  19885  iscyggen2  19913  iscyg3  19918  gsumval3lem1  19937  gsumval3  19939  dprdf1  20067  subgdmdprd  20068  subgdprd  20069  lindfmm  21864  m2cpmmhm  22766  leordtval2  23235  lecldbas  23242  discmp  23421  cmpsub  23423  tgcmp  23424  hauscmplem  23429  2ndcctbss  23478  2ndcsep  23482  comppfsc  23555  kgentop  23565  1stckgen  23577  kgencn2  23580  txuni2  23588  xkoopn  23612  xkouni  23622  xkoccn  23642  ptcnplem  23644  txkgen  23675  xkoco1cn  23680  xkoco2cn  23681  xkococnlem  23682  xkococn  23683  xkoinjcn  23710  hmphdis  23819  zfbas  23919  uzrest  23920  elfm  23970  alexsubALT  24074  efmndtmd  24124  submtmd  24127  symgtgp  24129  tsmsxplem1  24176  blin2  24454  imasf1oxms  24517  tgqioo  24835  xrtgioo  24841  metdscn2  24892  iimulcn  24980  iimulcnOLD  24981  icchmeo  24984  icchmeoOLD  24985  xrhmeo  24990  cnheiborlem  24999  tcphex  25264  tchnmfval  25275  fmcfil  25319  causs  25345  ovolficcss  25517  elovolm  25523  ovoliunlem2  25551  volsup  25604  uniioovol  25627  dyadmbllem  25647  dyadmbl  25648  opnmbllem  25649  opnmblALT  25651  volsup2  25653  mbfconstlem  25675  i1fd  25729  i1f1  25738  itg11  25739  itg1addlem4  25747  itg1addlem4OLD  25748  itg1climres  25763  itg2gt0  25809  limciun  25943  c1liplem1  26049  dvne0f1  26065  dvcnvrelem2  26071  dvcnvre  26072  mdeglt  26118  mdegxrcl  26120  mdegcl  26122  ig1peu  26228  ulmss  26454  reeff1o  26505  efifo  26603  dvlog  26707  efopn  26714  lgamcvg2  27112  dchrisum0fno1  27569  norn  27710  oldf  27910  usgredgss  29190  hhssims  31302  shsss  31341  pjrni  31730  imaelshi  32086  foresf1o  32531  fnpreimac  32687  tocyc01  33120  cycpmrn  33145  cycpmconjslem2  33157  cyc3conja  33159  dimkerim  33654  smatrcl  33756  locfinreflem  33800  esumcvg  34066  omssubadd  34281  sitgclbn  34324  eulerpartgbij  34353  eulerpartlemgvv  34357  eulerpartlemgf  34360  ballotlemsima  34496  lfuhgr  35101  mrsubf  35501  msubf  35516  mstapst  35531  mclsind  35554  mclsppslem  35567  icoreunrn  37341  pibt2  37399  ptrecube  37606  poimirlem1  37607  poimirlem3  37609  poimirlem12  37618  poimirlem16  37622  poimirlem32  37638  broucube  37640  heicant  37641  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  volsupnfl  37651  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  indexdom  37720  sstotbnd  37761  prdsbnd  37779  heibor1lem  37795  heiborlem1  37797  rrnval  37813  reheibor  37825  lsatset  38971  aks6d1c2  42111  aks6d1c6lem3  42153  aks6d1c6isolem1  42155  aks6d1c7lem1  42161  unitscyglem1  42176  elrfirn  42682  isnacs2  42693  nacsfix  42699  coeq0i  42740  diophrw  42746  dnwech  43036  pwssplit4  43077  hbt  43118  rnmptssf  45191  rnmptssff  45219  liminfval2  45723  fourierdlem12  46074  fourierdlem42  46104  fourierdlem54  46115  fourierdlem76  46137  fourierdlem85  46146  fourierdlem88  46149  fourierdlem93  46154  fourierdlem113  46174  hoicvr  46503  vonvolmbl2  46618  vonvol2  46619  fafvelcdm  47119  fafv2elcdm  47183  mgmplusfreseq  48008  elbigolo1  48406  aacllem  49031