Theorem frnd 6617

Description: Deduction form of frn 6616. 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 6616	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3888  ran crn 5591  ⟶wf 6433

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 397  df-f 6441

This theorem is referenced by:  f1un  6745  fliftrel  7188  f1iun  7795  f1dmex  7808  fo2ndf  7971  onoviun  8183  onnseq  8184  smores2  8194  domdifsn  8850  omxpenlem  8869  sucdom2OLD  8878  fodomr  8924  domss2  8932  f1domfi  8976  sucdom2  8998  f1finf1o  9055  f1fi  9115  unirnffid  9120  intrnfi  9184  dffi3  9199  ordtypelem8  9293  ordtypelem9  9294  ordtypelem10  9295  hartogslem1  9310  brwdom2  9341  unxpwdom2  9356  ixpiunwdom  9358  infdifsn  9424  cantnf  9460  ac10ct  9799  numacn  9814  infpwfien  9827  fictb  10010  isf34lem5  10143  isf34lem7  10144  isf34lem6  10145  enfin1ai  10149  canthp1lem2  10418  gch3  10441  wuncval2  10512  peano5nni  11985  hashimarn  14164  hashf1lem1  14177  hashf1lem1OLD  14178  hashf1lem2  14179  ccatrn  14303  swrdrn  14374  pfxrn  14407  cshwrn  14524  limsupgle  15195  limsupgre  15199  isercolllem2  15386  isercoll  15388  isercoll2  15389  climsup  15390  ruclem11  15958  4sqlem11  16665  vdwapf  16682  vdwlem11  16701  0ram  16730  funcres2b  17621  funcres2c  17626  setcepi  17812  yoniso  18012  isacs4lem  18271  mhmima  18472  gsumwspan  18494  frmdss2  18511  cycsubm  18830  cycsubgcl  18834  cycsubgss  18835  ghmrn  18856  conjnmz  18877  cntzmhm  18954  f1omvdconj  19063  odf1o2  19187  pgpssslw  19228  sylow2blem1  19234  lsmssv  19257  smndlsmidm  19270  lsmidmOLD  19278  pj1ghm2  19319  efgsp1  19352  efgrelexlemb  19365  cntzcmnf  19455  cyggenod  19493  gsumval3eu  19514  gsumval3lem2  19516  gsumval3  19517  gsumzsubmcl  19528  gsumzaddlem  19531  gsumzadd  19532  gsumzsplit  19537  gsumconst  19544  gsumzoppg  19554  gsumpt  19572  dmdprdd  19611  dprdfcntz  19627  dprdfeq0  19634  dprdlub  19638  dprdres  19640  dprdss  19641  dprdz  19642  subgdprd  19647  dprd2dlem1  19653  dprd2da  19654  dmdprdsplit2lem  19657  dpjghm2  19676  ablfac1b  19682  lmhmlsp  20320  pj1lmhm2  20372  pjfo  20931  frlmsplit2  20989  frlmsslsp  21012  frlmlbs  21013  frlmup3  21016  frlmup4  21017  lindff1  21036  lindfrn  21037  f1lindf  21038  indlcim  21056  aspval2  21111  mplcoe5lem  21249  mplbas2  21252  mplind  21287  evlslem1  21301  evlseu  21302  gsumply1subr  21414  m2cpmf1  21901  m2cpmghm  21902  iinopn  22060  pptbas  22167  tgrest  22319  resttopon  22321  rest0  22329  restfpw  22339  ordtbaslem  22348  ordtuni  22350  ordtbas2  22351  ordtrest  22362  ordtrest2  22364  cnclsi  22432  cnrest2r  22447  cnprest2  22450  lmss  22458  cncmp  22552  rncmp  22556  discmp  22558  connima  22585  conncn  22586  2ndcdisj  22616  2ndcomap  22618  dis2ndc  22620  lly1stc  22656  comppfsc  22692  kgencmp  22705  1stckgenlem  22713  kgencn3  22718  ptbasfi  22741  txbasval  22766  upxp  22783  uptx  22785  txtube  22800  txcmplem1  22801  txcmplem2  22802  tx1stc  22810  xkoptsub  22814  xkoco2cn  22818  xkococnlem  22819  hmeores  22931  fbasrn  23044  trfilss  23049  trfg  23051  uzrest  23057  rnelfmlem  23112  fclscmpi  23189  alexsublem  23204  ptcmplem1  23212  ptcmplem3  23214  cnextcn  23227  tmdgsum2  23256  subgtgp  23265  subgntr  23267  opnsubg  23268  clsnsg  23270  tgpconncomp  23273  tsmsfbas  23288  prdsdsf  23529  prdsxmetlem  23530  prdsmet  23532  imasdsf1olem  23535  unirnblps  23581  unirnbl  23582  prdsbl  23656  met1stc  23686  met2ndci  23687  prdsxmslem2  23694  xrge0gsumle  24005  xrge0tsms  24006  metdcn2  24011  metdsf  24020  metdsge  24021  cnmptre  24099  bndth  24130  evth  24131  evth2  24132  lebnumlem2  24134  lebnumlem3  24135  reparphti  24169  bcthlem5  24501  minveclem1  24597  minveclem3b  24601  evthicc2  24633  ovolmge0  24650  ovollb  24652  ovolgelb  24653  ovollb2lem  24661  ovollb2  24662  ovolunlem1a  24669  ovolunlem1  24670  ovoliunlem1  24675  ovoliun  24678  ovoliun2  24679  ovolscalem1  24686  ovolicc1  24689  ovolicc2lem4  24693  ovolicc2  24695  voliunlem2  24724  voliunlem3  24725  ioombl1lem2  24732  ioombl1lem4  24734  uniioovol  24752  uniiccvol  24753  uniioombllem1  24754  uniioombllem2  24756  uniioombllem3  24758  uniioombllem6  24761  uniioombl  24762  volsup2  24778  vitalilem2  24782  vitalilem4  24784  vitalilem5  24785  mbfsup  24837  mbfinf  24838  mbflimsup  24839  i1fima  24851  i1fima2  24852  itg1cl  24858  itg1ge0  24859  i1fmullem  24867  i1fadd  24868  i1fmul  24869  itg1addlem4  24872  itg1addlem4OLD  24873  itg1addlem5  24874  i1fmulc  24877  itg1mulc  24878  i1fres  24879  itg10a  24884  itg1ge0a  24885  itg1climres  24888  mbfi1fseqlem4  24892  itg2seq  24916  itg2monolem1  24924  itg2monolem2  24925  itg2monolem3  24926  itg2mono  24927  itg2i1fseq2  24930  itg2gt0  24934  itg2cnlem1  24935  itg2cn  24937  dvne0  25184  lhop2  25188  mdegleb  25238  mdegldg  25240  aalioulem3  25503  logccv  25827  efrlim  26128  basellem3  26241  fsumvma  26370  lgseisenlem4  26535  uhgredgn0  27507  upgredgss  27511  umgredgss  27512  edgupgr  27513  upgredg  27516  usgruspgrb  27560  upgrres1  27689  ubthlem1  29241  minvecolem1  29245  htthlem  29288  ofrn  30985  ofrn2  30986  xppreima2  30997  fsumiunle  31152  mgcf1o  31290  gsumhashmul  31325  xrge0tsmsd  31326  symgcom  31361  cycpmcl  31392  cycpmco2lem1  31402  cycpmco2lem5  31406  cycpmco2  31409  cycpmconjv  31418  cycpmconjslem2  31431  cmpcref  31809  ordtrestNEW  31880  ordtrest2NEW  31882  xrge0mulc1cn  31900  rge0scvg  31908  esumcst  32040  esumpfinvallem  32051  esumpcvgval  32055  esumiun  32071  omssubadd  32276  carsggect  32294  sibfinima  32315  sitgclg  32318  sitgaddlemb  32324  eulerpartgbij  32348  rrvrnss  32423  orvcval4  32436  erdsze2lem2  33175  cvxpconn  33213  cvxsconn  33214  cvmsss2  33245  cvmliftlem8  33263  cvmlift3lem6  33295  mrsubrn  33484  msubrn  33500  mvtss  33524  mclsssvlem  33533  mclsax  33540  mclsind  33541  neibastop2lem  34558  tailfb  34575  knoppcnlem10  34691  lindsdom  35780  poimirlem2  35788  poimirlem11  35797  poimirlem19  35805  poimirlem27  35813  poimirlem30  35816  mblfinlem2  35824  itg2addnclem2  35838  itg2gt0cn  35841  ftc1anclem3  35861  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anc  35867  cnresima  35931  istotbnd3  35938  sstotbnd2  35941  totbndbnd  35956  prdsbnd  35960  cntotbnd  35963  ismtyima  35970  heibor1lem  35976  heibor  35988  rrnequiv  36002  lsatlss  37017  cdleme50rnlem  38565  sticksstones2  40110  cmpfiiin  40526  isnacs3  40539  eldioph2lem2  40590  fnwe2lem2  40883  lmhmfgima  40916  gneispacern  41755  imo72b2lem0  41783  imo72b2lem2  41785  imo72b2lem1  41787  imo72b2  41790  refsumcn  42580  cncmpmax  42582  elpmrn  42767  climinf  43154  climinf2lem  43254  limsupvaluz2  43286  supcnvlimsup  43288  limsupgtlem  43325  icccncfext  43435  dvsinax  43461  itgsubsticclem  43523  fourierdlem70  43724  fourierdlem82  43736  fge0npnf  43912  sge0resrnlem  43948  sge0isum  43972  sge0seq  43991  meadjiunlem  44010  omeiunle  44062  hoicvr  44093  vonvolmbllem  44205  preimaioomnf  44264  smfco  44347  mgmhmima  45367  ackvalsucsucval  46045  aacllem  46516