Theorem frnd 6660

Description: Deduction form of frn 6659. The range of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
frnd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
frnd	⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)

Proof of Theorem frnd

Step	Hyp	Ref	Expression
1		frnd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		frn 6659	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3903  ran crn 5620  ⟶wf 6478

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 6486

This theorem is referenced by:  f1un  6784  fliftrel  7245  f1iun  7879  f1dmex  7892  fo2ndf  8054  onoviun  8266  onnseq  8267  smores2  8277  domdifsn  8977  omxpenlem  8995  fodomr  9045  domss2  9053  f1domfi  9095  sucdom2  9117  f1finf1o  9162  infn0  9191  f1fi  9203  fodomfir  9218  unirnffid  9237  intrnfi  9306  dffi3  9321  ordtypelem8  9417  ordtypelem9  9418  ordtypelem10  9419  hartogslem1  9434  brwdom2  9465  unxpwdom2  9480  ixpiunwdom  9482  infdifsn  9553  cantnf  9589  ac10ct  9928  numacn  9943  infpwfien  9956  fictb  10138  isf34lem5  10272  isf34lem7  10273  isf34lem6  10274  enfin1ai  10278  canthp1lem2  10547  gch3  10570  wuncval2  10641  peano5nni  12131  hashimarn  14347  hashf1lem1  14362  hashf1lem2  14363  ccatrn  14496  swrdrn  14559  pfxrn  14592  cshwrn  14708  limsupgle  15384  limsupgre  15388  isercolllem2  15573  isercoll  15575  isercoll2  15576  climsup  15577  ruclem11  16149  4sqlem11  16867  vdwapf  16884  vdwlem11  16903  0ram  16932  funcres2b  17804  funcres2c  17810  setcepi  17995  yoniso  18191  isacs4lem  18450  mgmhmima  18589  mhmima  18699  gsumwspan  18720  frmdss2  18737  cycsubm  19081  cycsubgcl  19085  cycsubgss  19086  ghmrn  19108  conjnmz  19131  ghmqusnsg  19161  ghmquskerlem3  19165  cntzmhm  19220  f1omvdconj  19325  odf1o2  19452  pgpssslw  19493  sylow2blem1  19499  lsmssv  19522  smndlsmidm  19535  pj1ghm2  19583  efgsp1  19616  efgrelexlemb  19629  cntzcmnf  19724  cyggenod  19763  gsumval3eu  19783  gsumval3lem2  19785  gsumval3  19786  gsumzsubmcl  19797  gsumzaddlem  19800  gsumzadd  19801  gsumzsplit  19806  gsumconst  19813  gsumzoppg  19823  gsumpt  19841  dmdprdd  19880  dprdfcntz  19896  dprdfeq0  19903  dprdlub  19907  dprdres  19909  dprdss  19910  dprdz  19911  subgdprd  19916  dprd2dlem1  19922  dprd2da  19923  dmdprdsplit2lem  19926  dpjghm2  19945  ablfac1b  19951  lmhmlsp  20953  pj1lmhm2  21005  pjfo  21622  frlmsplit2  21680  frlmsslsp  21703  frlmlbs  21704  frlmup3  21707  frlmup4  21708  lindff1  21727  lindfrn  21728  f1lindf  21729  indlcim  21747  aspval2  21805  mplcoe5lem  21944  mplbas2  21947  mplind  21975  evlslem1  21987  evlseu  21988  gsumply1subr  22116  m2cpmf1  22628  m2cpmghm  22629  iinopn  22787  pptbas  22893  tgrest  23044  resttopon  23046  rest0  23054  restfpw  23064  ordtbaslem  23073  ordtuni  23075  ordtbas2  23076  ordtrest  23087  ordtrest2  23089  cnclsi  23157  cnrest2r  23172  cnprest2  23175  lmss  23183  cncmp  23277  rncmp  23281  discmp  23283  connima  23310  conncn  23311  2ndcdisj  23341  2ndcomap  23343  dis2ndc  23345  lly1stc  23381  comppfsc  23417  kgencmp  23430  1stckgenlem  23438  kgencn3  23443  ptbasfi  23466  txbasval  23491  upxp  23508  uptx  23510  txtube  23525  txcmplem1  23526  txcmplem2  23527  tx1stc  23535  xkoptsub  23539  xkoco2cn  23543  xkococnlem  23544  hmeores  23656  fbasrn  23769  trfilss  23774  trfg  23776  uzrest  23782  rnelfmlem  23837  fclscmpi  23914  alexsublem  23929  ptcmplem1  23937  ptcmplem3  23939  cnextcn  23952  tmdgsum2  23981  subgtgp  23990  subgntr  23992  opnsubg  23993  clsnsg  23995  tgpconncomp  23998  tsmsfbas  24013  prdsdsf  24253  prdsxmetlem  24254  prdsmet  24256  imasdsf1olem  24259  unirnblps  24305  unirnbl  24306  prdsbl  24377  met1stc  24407  met2ndci  24408  prdsxmslem2  24415  xrge0gsumle  24720  xrge0tsms  24721  metdcn2  24726  metdsf  24735  metdsge  24736  cnmptre  24819  bndth  24855  evth  24856  evth2  24857  lebnumlem2  24859  lebnumlem3  24860  reparphti  24894  reparphtiOLD  24895  bcthlem5  25226  minveclem1  25322  minveclem3b  25326  evthicc2  25359  ovolmge0  25376  ovollb  25378  ovolgelb  25379  ovollb2lem  25387  ovollb2  25388  ovolunlem1a  25395  ovolunlem1  25396  ovoliunlem1  25401  ovoliun  25404  ovoliun2  25405  ovolscalem1  25412  ovolicc1  25415  ovolicc2lem4  25419  ovolicc2  25421  voliunlem2  25450  voliunlem3  25451  ioombl1lem2  25458  ioombl1lem4  25460  uniioovol  25478  uniiccvol  25479  uniioombllem1  25480  uniioombllem2  25482  uniioombllem3  25484  uniioombllem6  25487  uniioombl  25488  volsup2  25504  vitalilem2  25508  vitalilem4  25510  vitalilem5  25511  mbfsup  25563  mbfinf  25564  mbflimsup  25565  i1fima  25577  i1fima2  25578  itg1cl  25584  itg1ge0  25585  i1fmullem  25593  i1fadd  25594  i1fmul  25595  itg1addlem4  25598  itg1addlem5  25599  i1fmulc  25602  itg1mulc  25603  i1fres  25604  itg10a  25609  itg1ge0a  25610  itg1climres  25613  mbfi1fseqlem4  25617  itg2seq  25641  itg2monolem1  25649  itg2monolem2  25650  itg2monolem3  25651  itg2mono  25652  itg2i1fseq2  25655  itg2gt0  25659  itg2cnlem1  25660  itg2cn  25662  dvne0  25914  lhop2  25918  mdegleb  25967  mdegldg  25969  aalioulem3  26240  logccv  26570  efrlim  26877  efrlimOLD  26878  basellem3  26991  fsumvma  27122  lgseisenlem4  27287  noseqind  28191  uhgredgn0  29073  upgredgss  29077  umgredgss  29078  edgupgr  29079  upgredg  29082  usgruspgrb  29128  upgrres1  29258  ubthlem1  30814  minvecolem1  30818  htthlem  30861  ofrn  32582  ofrn2  32583  xppreima2  32594  fsumiunle  32774  ccatws1f1olast  32894  mgcf1o  32945  chnso  32956  gsumhashmul  33014  xrge0tsmsd  33015  symgcom  33025  cycpmcl  33058  cycpmco2lem1  33068  cycpmco2lem5  33072  cycpmco2  33075  cycpmconjv  33084  cycpmconjslem2  33097  elrgspnsubrunlem2  33188  idomsubr  33248  1arithidom  33474  psrbasfsupp  33544  ply1degltdimlem  33589  cmpcref  33817  ordtrestNEW  33888  ordtrest2NEW  33890  xrge0mulc1cn  33908  rge0scvg  33916  esumcst  34030  esumpfinvallem  34041  esumpcvgval  34045  esumiun  34061  omssubadd  34268  carsggect  34286  sibfinima  34307  sitgclg  34310  sitgaddlemb  34316  eulerpartgbij  34340  rrvrnss  34415  orvcval4  34429  erdsze2lem2  35181  cvxpconn  35219  cvxsconn  35220  cvmsss2  35251  cvmliftlem8  35269  cvmlift3lem6  35301  mrsubrn  35490  msubrn  35506  mvtss  35530  mclsssvlem  35539  mclsax  35546  mclsind  35547  neibastop2lem  36338  tailfb  36355  knoppcnlem10  36480  lindsdom  37598  poimirlem2  37606  poimirlem11  37615  poimirlem19  37623  poimirlem27  37631  poimirlem30  37634  mblfinlem2  37642  itg2addnclem2  37656  itg2gt0cn  37659  ftc1anclem3  37679  ftc1anclem6  37682  ftc1anclem7  37683  ftc1anc  37685  cnresima  37748  istotbnd3  37755  sstotbnd2  37758  totbndbnd  37773  prdsbnd  37777  cntotbnd  37780  ismtyima  37787  heibor1lem  37793  heibor  37805  rrnequiv  37819  lsatlss  38979  cdleme50rnlem  40527  sticksstones2  42124  aks6d1c6lem5  42154  cmpfiiin  42674  isnacs3  42687  eldioph2lem2  42738  fnwe2lem2  43028  lmhmfgima  43061  cantnfub2  43299  onnog  43406  gneispacern  44115  imo72b2lem2  44144  imo72b2lem1  44146  imo72b2  44149  refsumcn  45012  cncmpmax  45014  elpmrn  45202  climinf  45591  climinf2lem  45691  limsupvaluz2  45723  supcnvlimsup  45725  limsupgtlem  45762  icccncfext  45872  dvsinax  45898  itgsubsticclem  45960  fourierdlem70  46161  fourierdlem82  46173  fge0npnf  46352  sge0resrnlem  46388  sge0isum  46412  sge0seq  46431  meadjiunlem  46450  omeiunle  46502  hoicvr  46533  vonvolmbllem  46645  preimaioomnf  46704  smfco  46787  ackvalsucsucval  48677  aacllem  49790