Theorem frn 6722

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

Syntax hints:   → wi 4   ⊆ wss 3948  ran crn 5677   Fn wfn 6536  ⟶wf 6537

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 398  df-f 6545

This theorem is referenced by:  frnd  6723  fimass  6736  fimacnv  6737  fco2  6742  fssxp  6743  fimacnvdisj  6767  f00  6771  f0rn0  6774  f1resf1  6794  foconst  6818  ffvelcdm  7081  f1ompt  7108  fnfvrnss  7117  rnmptss  7119  isofr2  7338  fiun  7926  fo1stres  7998  fo2ndres  7999  1stcof  8002  2ndcof  8003  fnwelem  8114  orderseqlem  8140  tposf2  8232  seqomlem2  8448  oacomf1olem  8561  naddunif  8689  naddasslem1  8690  naddasslem2  8691  map0b  8874  mapsnd  8877  fipreima  9355  indexfi  9357  dffi3  9423  oismo  9532  djuin  9910  updjudhcoinlf  9924  updjudhcoinrg  9925  acndom  10043  acndom2  10046  dfac12lem2  10136  dfac12lem3  10137  ackbij1  10230  cfflb  10251  fin23lem40  10343  fin23lem41  10344  isf34lem7  10371  fin1a2lem6  10397  fin1a2lem7  10398  hsmexlem4  10421  hsmexlem5  10422  axdc2lem  10440  axdc3lem2  10443  ttukeylem6  10506  unirnfdomd  10559  pwcfsdom  10575  smobeth  10578  pwfseqlem5  10655  tskurn  10781  wfgru  10808  rpnnen1lem4  12961  rpnnen1lem5  12962  unirnioo  13423  fseqsupcl  13939  fseqsupubi  13940  limsupcl  15414  limsuple  15419  limsupval2  15421  prmreclem6  16851  0ram2  16951  0ramcl  16953  imasdsval2  17459  mrcssv  17555  isacs1i  17598  acsmapd  18504  acsmap2d  18505  gsumval1  18599  dfod2  19427  odcl2  19428  sylow1lem2  19462  efgsfo  19602  gexex  19716  iscyggen2  19744  iscyg3  19749  gsumval3lem1  19768  gsumval3  19770  dprdf1  19898  subgdmdprd  19899  subgdprd  19900  lindfmm  21374  m2cpmmhm  22239  leordtval2  22708  lecldbas  22715  discmp  22894  cmpsub  22896  tgcmp  22897  hauscmplem  22902  2ndcctbss  22951  2ndcsep  22955  comppfsc  23028  kgentop  23038  1stckgen  23050  kgencn2  23053  txuni2  23061  xkoopn  23085  xkouni  23095  xkoccn  23115  ptcnplem  23117  txkgen  23148  xkoco1cn  23153  xkoco2cn  23154  xkococnlem  23155  xkococn  23156  xkoinjcn  23183  hmphdis  23292  zfbas  23392  uzrest  23393  elfm  23443  alexsubALT  23547  efmndtmd  23597  submtmd  23600  symgtgp  23602  tsmsxplem1  23649  blin2  23927  imasf1oxms  23990  tgqioo  24308  xrtgioo  24314  metdscn2  24365  iimulcn  24446  icchmeo  24449  xrhmeo  24454  cnheiborlem  24462  tcphex  24726  tchnmfval  24737  fmcfil  24781  causs  24807  ovolficcss  24978  elovolm  24984  ovoliunlem2  25012  volsup  25065  uniioovol  25088  dyadmbllem  25108  dyadmbl  25109  opnmbllem  25110  opnmblALT  25112  volsup2  25114  mbfconstlem  25136  i1fd  25190  i1f1  25199  itg11  25200  itg1addlem4  25208  itg1addlem4OLD  25209  itg1climres  25224  itg2gt0  25270  limciun  25403  c1liplem1  25505  dvne0f1  25521  dvcnvrelem2  25527  dvcnvre  25528  mdeglt  25575  mdegxrcl  25577  mdegcl  25579  ig1peu  25681  ulmss  25901  reeff1o  25951  efifo  26048  dvlog  26151  efopn  26158  lgamcvg2  26549  dchrisum0fno1  27004  norn  27144  oldf  27342  usgredgss  28409  hhssims  30515  shsss  30554  pjrni  30943  imaelshi  31299  foresf1o  31730  fnpreimac  31884  tocyc01  32265  cycpmrn  32290  cycpmconjslem2  32302  cyc3conja  32304  dimkerim  32701  smatrcl  32765  locfinreflem  32809  esumcvg  33073  omssubadd  33288  sitgclbn  33331  eulerpartgbij  33360  eulerpartlemgvv  33364  eulerpartlemgf  33367  ballotlemsima  33503  hashf1dmcdm  34094  lfuhgr  34097  mrsubf  34497  msubf  34512  mstapst  34527  mclsind  34550  mclsppslem  34563  gg-iimulcn  35158  gg-icchmeo  35159  icoreunrn  36229  pibt2  36287  ptrecube  36477  poimirlem1  36478  poimirlem3  36480  poimirlem12  36489  poimirlem16  36493  poimirlem32  36509  broucube  36511  heicant  36512  opnmbllem0  36513  mblfinlem1  36514  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  volsupnfl  36522  ftc1anclem5  36554  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  indexdom  36591  sstotbnd  36632  prdsbnd  36650  heibor1lem  36666  heiborlem1  36668  rrnval  36684  reheibor  36696  lsatset  37849  elrfirn  41419  isnacs2  41430  nacsfix  41436  coeq0i  41477  diophrw  41483  dnwech  41776  pwssplit4  41817  hbt  41858  rnmptssf  43938  rnmptssff  43966  liminfval2  44471  fourierdlem12  44822  fourierdlem42  44852  fourierdlem54  44863  fourierdlem76  44885  fourierdlem85  44894  fourierdlem88  44897  fourierdlem93  44902  fourierdlem113  44922  hoicvr  45251  vonvolmbl2  45366  vonvol2  45367  fafvelcdm  45865  fafv2elcdm  45929  mgmplusfreseq  46530  elbigolo1  47197  aacllem  47802