Theorem frn 6717

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895  ran crn 5651   Fn wfn 6533  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6542

This theorem is used by:  frnd  6718  fimass  6730  fimacnv  6732  fco2  6736  fssxp  6737  fimacnvdisj  6760  f00  6764  f0rn0  6767  f1resf1  6788  foconst  6811  ffvelcdm  7081  f1ompt  7111  fnfvrnss  7121  rnmptss  7123  isofr2  7352  f1we  7363  fiun  7955  fo1stres  8027  fo2ndres  8028  1stcof  8031  2ndcof  8032  fnwelem  8143  orderseqlem  8174  tposf2  8267  seqomlem2  8461  oacomf1olem  8572  naddunif  8703  naddasslem1  8704  naddasslem2  8705  map0b  8911  mapsnd  8914  fipreima  9347  indexfi  9349  dffi3  9423  oismo  9534  djuin  9999  updjudhcoinlf  10013  updjudhcoinrg  10014  acndom  10130  acndom2  10133  dfac12lem2  10223  dfac12lem3  10224  ackbij1  10315  cfflb  10337  fin23lem40  10429  fin23lem41  10430  isf34lem7  10457  fin1a2lem6  10483  fin1a2lem7  10484  hsmexlem4  10507  hsmexlem5  10508  axdc2lem  10526  axdc3lem2  10529  ttukeylem6  10592  unirnfdomd  10652  pwcfsdom  10668  smobeth  10671  pwfseqlem5  10748  tskurn  10874  wfgru  10901  rpnnen1lem4  13108  rpnnen1lem5  13109  unirnioo  13580  fseqsupcl  14120  fseqsupubi  14121  hashf1dmcdm  14589  limsupcl  15640  limsuple  15645  limsupval2  15647  prmreclem6  17099  0ram2  17199  0ramcl  17201  imasdsval2  17688  mrcssv  17788  isacs1i  17831  acsmapd  18728  acsmap2d  18729  gsumval1  18872  dfod2  19778  odcl2  19779  sylow1lem2  19813  efgsfo  19953  gexex  20067  iscyggen2  20095  iscyg3  20100  gsumval3lem1  20119  gsumval3  20121  dprdf1  20249  subgdmdprd  20250  subgdprd  20251  lindfmm  22133  m2cpmmhm  23063  leordtval2  23530  lecldbas  23537  discmp  23716  cmpsub  23718  tgcmp  23719  hauscmplem  23724  2ndcctbss  23774  2ndcsep  23778  comppfsc  23851  kgentop  23861  1stckgen  23873  kgencn2  23876  txuni2  23884  xkoopn  23908  xkouni  23918  xkoccn  23938  ptcnplem  23940  txkgen  23971  xkoco1cn  23976  xkoco2cn  23977  xkococnlem  23978  xkococn  23979  xkoinjcn  24006  hmphdis  24115  zfbas  24215  uzrest  24216  elfm  24266  alexsubALT  24370  efmndtmd  24420  submtmd  24423  symgtgp  24425  tsmsxplem1  24472  blin2  24748  imasf1oxms  24808  tgqioo  25119  xrtgioo  25126  metdscn2  25177  iimulcn  25259  icchmeo  25262  xrhmeo  25267  cnheiborlem  25275  tcphex  25538  tchnmfval  25549  fmcfil  25593  causs  25619  ovolficcss  25790  elovolm  25796  ovoliunlem2  25824  volsup  25877  uniioovol  25900  dyadmbllem  25920  dyadmbl  25921  opnmbllem  25922  opnmblALT  25924  volsup2  25926  mbfconstlem  25948  i1fd  26002  i1f1  26011  itg11  26012  itg1addlem4  26020  itg1climres  26035  itg2gt0  26081  limciun  26214  c1liplem1  26316  dvne0f1  26332  dvcnvrelem2  26338  dvcnvre  26339  mdeglt  26383  mdegxrcl  26385  mdegcl  26387  ig1peu  26493  ulmss  26724  reeff1o  26774  efifo  26875  dvlog  26979  efopn  26986  lgamcvg2  27382  dchrisum0fno1  27838  norn  28008  oldf  28223  lfuhgr  29726  usgredgss  29740  hhssims  31876  shsss  31915  pjrni  32304  imaelshi  32660  foresf1o  33100  fnpreimac  33264  tocyc01  33679  cycpmrn  33704  cycpmconjslem2  33716  cyc3conja  33718  dimkerim  34259  smatrcl  34428  locfinreflem  34472  esumcvg  34718  omssubadd  34932  sitgclbn  34975  eulerpartgbij  35004  eulerpartlemgvv  35008  eulerpartlemgf  35011  ballotlemsima  35148  acwer1prc  35760  mrsubf  36282  msubf  36297  mstapst  36312  mclsind  36335  mclsppslem  36348  icoreunrn  38283  pibt2  38341  ptrecube  38539  poimirlem1  38540  poimirlem3  38542  poimirlem12  38551  poimirlem16  38555  poimirlem32  38571  broucube  38573  heicant  38574  opnmbllem0  38575  mblfinlem1  38576  mblfinlem2  38577  mblfinlem3  38578  mblfinlem4  38579  ismblfin  38580  volsupnfl  38584  ftc1anclem5  38616  ftc1anclem7  38618  ftc1anclem8  38619  ftc1anc  38620  indexdom  38669  sstotbnd  38710  prdsbnd  38728  heibor1lem  38744  heiborlem1  38746  rrnval  38762  reheibor  38774  lsatset  40048  aks6d1c2  43181  aks6d1c6lem3  43223  aks6d1c6isolem1  43225  aks6d1c7lem1  43231  unitscyglem1  43246  elrfirn  43706  isnacs2  43717  nacsfix  43723  coeq0i  43764  diophrw  43770  pwssplit4  44091  hbt  44132  rnmptssf  46259  rnmptssff  46286  liminfval2  46778  fourierdlem12  47129  fourierdlem42  47159  fourierdlem54  47170  fourierdlem76  47192  fourierdlem85  47201  fourierdlem88  47204  fourierdlem93  47209  hoicvr  47558  vonvolmbl2  47673  vonvol2  47674  fafvelcdm  48240  fafv2elcdm  48304  mgmplusfreseq  49262  elbigolo1  49669  aacllem  50939