Theorem frnd 6676

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

Syntax hints:   → wi 4   ⊆ wss 3889  ran crn 5632  ⟶wf 6494

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 6502

This theorem is referenced by:  f1un  6800  fliftrel  7263  f1iun  7897  f1dmex  7910  fo2ndf  8071  onoviun  8283  onnseq  8284  smores2  8294  domdifsn  8998  omxpenlem  9016  fodomr  9066  domss2  9074  f1domfi  9115  sucdom2  9137  f1finf1o  9183  infn0  9212  f1fi  9224  fodomfir  9238  unirnffid  9257  intrnfi  9329  dffi3  9344  ordtypelem8  9440  ordtypelem9  9441  ordtypelem10  9442  hartogslem1  9457  brwdom2  9488  unxpwdom2  9503  ixpiunwdom  9505  infdifsn  9578  cantnf  9614  ac10ct  9956  numacn  9971  infpwfien  9984  fictb  10166  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  enfin1ai  10306  canthp1lem2  10576  gch3  10599  wuncval2  10670  peano5nni  12177  hashimarn  14402  hashf1lem1  14417  hashf1lem2  14418  ccatrn  14552  swrdrn  14615  pfxrn  14648  cshwrn  14764  limsupgle  15439  limsupgre  15443  isercolllem2  15628  isercoll  15630  isercoll2  15631  climsup  15632  ruclem11  16207  4sqlem11  16926  vdwapf  16943  vdwlem11  16962  0ram  16991  funcres2b  17864  funcres2c  17870  setcepi  18055  yoniso  18251  isacs4lem  18510  chnso  18590  mgmhmima  18683  mhmima  18793  gsumwspan  18814  frmdss2  18831  cycsubm  19177  cycsubgcl  19181  cycsubgss  19182  ghmrn  19204  conjnmz  19227  ghmqusnsg  19257  ghmquskerlem3  19261  cntzmhm  19316  f1omvdconj  19421  odf1o2  19548  pgpssslw  19589  sylow2blem1  19595  lsmssv  19618  smndlsmidm  19631  pj1ghm2  19679  efgsp1  19712  efgrelexlemb  19725  cntzcmnf  19820  cyggenod  19859  gsumval3eu  19879  gsumval3lem2  19881  gsumval3  19882  gsumzsubmcl  19893  gsumzaddlem  19896  gsumzadd  19897  gsumzsplit  19902  gsumconst  19909  gsumzoppg  19919  gsumpt  19937  dmdprdd  19976  dprdfcntz  19992  dprdfeq0  19999  dprdlub  20003  dprdres  20005  dprdss  20006  dprdz  20007  subgdprd  20012  dprd2dlem1  20018  dprd2da  20019  dmdprdsplit2lem  20022  dpjghm2  20041  ablfac1b  20047  lmhmlsp  21044  pj1lmhm2  21096  pjfo  21695  frlmsplit2  21753  frlmsslsp  21776  frlmlbs  21777  frlmup3  21780  frlmup4  21781  lindff1  21800  lindfrn  21801  f1lindf  21802  indlcim  21820  aspval2  21878  mplcoe5lem  22017  mplbas2  22020  mplind  22048  evlslem1  22060  evlseu  22061  gsumply1subr  22197  m2cpmf1  22708  m2cpmghm  22709  iinopn  22867  pptbas  22973  tgrest  23124  resttopon  23126  rest0  23134  restfpw  23144  ordtbaslem  23153  ordtuni  23155  ordtbas2  23156  ordtrest  23167  ordtrest2  23169  cnclsi  23237  cnrest2r  23252  cnprest2  23255  lmss  23263  cncmp  23357  rncmp  23361  discmp  23363  connima  23390  conncn  23391  2ndcdisj  23421  2ndcomap  23423  dis2ndc  23425  lly1stc  23461  comppfsc  23497  kgencmp  23510  1stckgenlem  23518  kgencn3  23523  ptbasfi  23546  txbasval  23571  upxp  23588  uptx  23590  txtube  23605  txcmplem1  23606  txcmplem2  23607  tx1stc  23615  xkoptsub  23619  xkoco2cn  23623  xkococnlem  23624  hmeores  23736  fbasrn  23849  trfilss  23854  trfg  23856  uzrest  23862  rnelfmlem  23917  fclscmpi  23994  alexsublem  24009  ptcmplem1  24017  ptcmplem3  24019  cnextcn  24032  tmdgsum2  24061  subgtgp  24070  subgntr  24072  opnsubg  24073  clsnsg  24075  tgpconncomp  24078  tsmsfbas  24093  prdsdsf  24332  prdsxmetlem  24333  prdsmet  24335  imasdsf1olem  24338  unirnblps  24384  unirnbl  24385  prdsbl  24456  met1stc  24486  met2ndci  24487  prdsxmslem2  24494  xrge0gsumle  24799  xrge0tsms  24800  metdcn2  24805  metdsf  24814  metdsge  24815  cnmptre  24894  bndth  24925  evth  24926  evth2  24927  lebnumlem2  24929  lebnumlem3  24930  reparphti  24964  bcthlem5  25295  minveclem1  25391  minveclem3b  25395  evthicc2  25427  ovolmge0  25444  ovollb  25446  ovolgelb  25447  ovollb2lem  25455  ovollb2  25456  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliun  25472  ovoliun2  25473  ovolscalem1  25480  ovolicc1  25483  ovolicc2lem4  25487  ovolicc2  25489  voliunlem2  25518  voliunlem3  25519  ioombl1lem2  25526  ioombl1lem4  25528  uniioovol  25546  uniiccvol  25547  uniioombllem1  25548  uniioombllem2  25550  uniioombllem3  25552  uniioombllem6  25555  uniioombl  25556  volsup2  25572  vitalilem2  25576  vitalilem4  25578  vitalilem5  25579  mbfsup  25631  mbfinf  25632  mbflimsup  25633  i1fima  25645  i1fima2  25646  itg1cl  25652  itg1ge0  25653  i1fmullem  25661  i1fadd  25662  i1fmul  25663  itg1addlem4  25666  itg1addlem5  25667  i1fmulc  25670  itg1mulc  25671  i1fres  25672  itg10a  25677  itg1ge0a  25678  itg1climres  25681  mbfi1fseqlem4  25685  itg2seq  25709  itg2monolem1  25717  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  itg2i1fseq2  25723  itg2gt0  25727  itg2cnlem1  25728  itg2cn  25730  dvne0  25978  lhop2  25982  mdegleb  26029  mdegldg  26031  aalioulem3  26300  logccv  26627  efrlim  26933  basellem3  27046  fsumvma  27176  lgseisenlem4  27341  noseqind  28284  uhgredgn0  29197  upgredgss  29201  umgredgss  29202  edgupgr  29203  upgredg  29206  usgruspgrb  29252  upgrres1  29382  ubthlem1  30941  minvecolem1  30945  htthlem  30988  ofrn  32712  ofrn2  32713  xppreima2  32724  fsumiunle  32902  ccatws1f1olast  33012  mgcf1o  33063  gsumhashmul  33128  xrge0tsmsd  33134  symgcom  33144  cycpmcl  33177  cycpmco2lem1  33187  cycpmco2lem5  33191  cycpmco2  33194  cycpmconjv  33203  cycpmconjslem2  33216  elrgspnsubrunlem2  33309  idomsubr  33370  1arithidom  33597  psrbasfsupp  33672  esplyfv  33714  esplyfval3  33716  ply1degltdimlem  33766  cmpcref  33994  ordtrestNEW  34065  ordtrest2NEW  34067  xrge0mulc1cn  34085  rge0scvg  34093  esumcst  34207  esumpfinvallem  34218  esumpcvgval  34222  esumiun  34238  omssubadd  34444  carsggect  34462  sibfinima  34483  sitgclg  34486  sitgaddlemb  34492  eulerpartgbij  34516  rrvrnss  34591  orvcval4  34605  erdsze2lem2  35386  cvxpconn  35424  cvxsconn  35425  cvmsss2  35456  cvmliftlem8  35474  cvmlift3lem6  35506  mrsubrn  35695  msubrn  35711  mvtss  35735  mclsssvlem  35744  mclsax  35751  mclsind  35752  neibastop2lem  36542  tailfb  36559  knoppcnlem10  36762  lindsdom  37935  poimirlem2  37943  poimirlem11  37952  poimirlem19  37960  poimirlem27  37968  poimirlem30  37971  mblfinlem2  37979  itg2addnclem2  37993  itg2gt0cn  37996  ftc1anclem3  38016  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anc  38022  cnresima  38085  istotbnd3  38092  sstotbnd2  38095  totbndbnd  38110  prdsbnd  38114  cntotbnd  38117  ismtyima  38124  heibor1lem  38130  heibor  38142  rrnequiv  38156  lsatlss  39442  cdleme50rnlem  40990  sticksstones2  42586  aks6d1c6lem5  42616  cmpfiiin  43129  isnacs3  43142  eldioph2lem2  43193  fnwe2lem2  43479  lmhmfgima  43512  cantnfub2  43750  onnoxpg  43856  gneispacern  44565  imo72b2lem2  44594  imo72b2lem1  44596  imo72b2  44599  refsumcn  45461  cncmpmax  45463  elpmrn  45649  climinf  46036  climinf2lem  46134  limsupvaluz2  46166  supcnvlimsup  46168  limsupgtlem  46205  icccncfext  46315  dvsinax  46341  itgsubsticclem  46403  fourierdlem70  46604  fourierdlem82  46616  fge0npnf  46795  sge0resrnlem  46831  sge0isum  46855  sge0seq  46874  meadjiunlem  46893  omeiunle  46945  hoicvr  46976  vonvolmbllem  47088  preimaioomnf  47147  smfco  47230  chnsubseqwl  47309  ackvalsucsucval  49164  aacllem  50276