Theorem frn 6701

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

Syntax hints:   → wi 4   ⊆ wss 3906  ran crn 5650   Fn wfn 6518  ⟶wf 6519

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 209  df-an 400  df-f 6527

This theorem is referenced by:  frnd  6702  fimass  6714  fimacnv  6716  fco2  6720  fssxp  6721  fimacnvdisj  6744  f00  6748  f0rn0  6751  f1resf1  6772  foconst  6795  ffvelcdm  7064  f1ompt  7094  fnfvrnss  7104  rnmptss  7106  isofr2  7330  fiun  7926  fo1stres  7998  fo2ndres  7999  1stcof  8002  2ndcof  8003  fnwelem  8113  orderseqlem  8139  tposf2  8232  seqomlem2  8424  oacomf1olem  8535  naddunif  8666  naddasslem1  8667  naddasslem2  8668  map0b  8867  mapsnd  8870  fipreima  9303  indexfi  9305  dffi3  9379  oismo  9490  djuin  9878  updjudhcoinlf  9892  updjudhcoinrg  9893  acndom  10009  acndom2  10012  dfac12lem2  10103  dfac12lem3  10104  ackbij1  10195  cfflb  10218  fin23lem40  10310  fin23lem41  10311  isf34lem7  10338  fin1a2lem6  10364  fin1a2lem7  10365  hsmexlem4  10388  hsmexlem5  10389  axdc2lem  10407  axdc3lem2  10410  ttukeylem6  10473  unirnfdomd  10527  pwcfsdom  10543  smobeth  10546  pwfseqlem5  10623  tskurn  10749  wfgru  10776  rpnnen1lem4  12983  rpnnen1lem5  12984  unirnioo  13455  fseqsupcl  13992  fseqsupubi  13993  hashf1dmcdm  14459  limsupcl  15502  limsuple  15507  limsupval2  15509  prmreclem6  16959  0ram2  17059  0ramcl  17061  imasdsval2  17548  mrcssv  17648  isacs1i  17691  acsmapd  18588  acsmap2d  18589  gsumval1  18719  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  21881  m2cpmmhm  22807  leordtval2  23274  lecldbas  23281  discmp  23460  cmpsub  23462  tgcmp  23463  hauscmplem  23468  2ndcctbss  23517  2ndcsep  23521  comppfsc  23594  kgentop  23604  1stckgen  23616  kgencn2  23619  txuni2  23627  xkoopn  23651  xkouni  23661  xkoccn  23681  ptcnplem  23683  txkgen  23714  xkoco1cn  23719  xkoco2cn  23720  xkococnlem  23721  xkococn  23722  xkoinjcn  23749  hmphdis  23858  zfbas  23958  uzrest  23959  elfm  24009  alexsubALT  24113  efmndtmd  24163  submtmd  24166  symgtgp  24168  tsmsxplem1  24215  blin2  24491  imasf1oxms  24551  tgqioo  24862  xrtgioo  24869  metdscn2  24920  iimulcn  25002  icchmeo  25005  xrhmeo  25010  cnheiborlem  25018  tcphex  25281  tchnmfval  25292  fmcfil  25336  causs  25362  ovolficcss  25533  elovolm  25539  ovoliunlem2  25567  volsup  25620  uniioovol  25643  dyadmbllem  25663  dyadmbl  25664  opnmbllem  25665  opnmblALT  25667  volsup2  25669  mbfconstlem  25691  i1fd  25745  i1f1  25754  itg11  25755  itg1addlem4  25763  itg1climres  25778  itg2gt0  25824  limciun  25958  c1liplem1  26060  dvne0f1  26076  dvcnvrelem2  26082  dvcnvre  26083  mdeglt  26127  mdegxrcl  26129  mdegcl  26131  ig1peu  26237  ulmss  26462  reeff1o  26512  efifo  26614  dvlog  26718  efopn  26725  lgamcvg2  27121  dchrisum0fno1  27577  norn  27717  oldf  27932  usgredgss  29362  hhssims  31479  shsss  31518  pjrni  31907  imaelshi  32263  foresf1o  32705  fnpreimac  32874  tocyc01  33300  cycpmrn  33325  cycpmconjslem2  33337  cyc3conja  33339  dimkerim  33926  smatrcl  34095  locfinreflem  34139  esumcvg  34385  omssubadd  34599  sitgclbn  34642  eulerpartgbij  34671  eulerpartlemgvv  34675  eulerpartlemgf  34678  ballotlemsima  34815  lfuhgr  35473  mrsubf  35872  msubf  35887  mstapst  35902  mclsind  35925  mclsppslem  35938  icoreunrn  37858  pibt2  37916  ptrecube  38124  poimirlem1  38125  poimirlem3  38127  poimirlem12  38136  poimirlem16  38140  poimirlem32  38156  broucube  38158  heicant  38159  opnmbllem0  38160  mblfinlem1  38161  mblfinlem2  38162  mblfinlem3  38163  mblfinlem4  38164  ismblfin  38165  volsupnfl  38169  ftc1anclem5  38201  ftc1anclem7  38203  ftc1anclem8  38204  ftc1anc  38205  indexdom  38238  sstotbnd  38279  prdsbnd  38297  heibor1lem  38313  heiborlem1  38315  rrnval  38331  reheibor  38343  lsatset  39619  aks6d1c2  42752  aks6d1c6lem3  42794  aks6d1c6isolem1  42796  aks6d1c7lem1  42802  unitscyglem1  42817  elrfirn  43281  isnacs2  43292  nacsfix  43298  coeq0i  43339  diophrw  43345  dnwech  43630  pwssplit4  43671  hbt  43712  rnmptssf  45827  rnmptssff  45854  liminfval2  46347  fourierdlem12  46698  fourierdlem42  46728  fourierdlem54  46739  fourierdlem76  46761  fourierdlem85  46770  fourierdlem88  46773  fourierdlem93  46778  hoicvr  47127  vonvolmbl2  47242  vonvol2  47243  fafvelcdm  47769  fafv2elcdm  47833  mgmplusfreseq  48792  elbigolo1  49184  aacllem  50427