Theorem frnd 6678

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

Syntax hints:   → wi 4   ⊆ wss 3903  ran crn 5633  ⟶wf 6496

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 6504

This theorem is referenced by:  f1un  6802  fliftrel  7264  f1iun  7898  f1dmex  7911  fo2ndf  8073  onoviun  8285  onnseq  8286  smores2  8296  domdifsn  9000  omxpenlem  9018  fodomr  9068  domss2  9076  f1domfi  9117  sucdom2  9139  f1finf1o  9185  infn0  9214  f1fi  9226  fodomfir  9240  unirnffid  9259  intrnfi  9331  dffi3  9346  ordtypelem8  9442  ordtypelem9  9443  ordtypelem10  9444  hartogslem1  9459  brwdom2  9490  unxpwdom2  9505  ixpiunwdom  9507  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  12160  hashimarn  14375  hashf1lem1  14390  hashf1lem2  14391  ccatrn  14525  swrdrn  14588  pfxrn  14621  cshwrn  14737  limsupgle  15412  limsupgre  15416  isercolllem2  15601  isercoll  15603  isercoll2  15604  climsup  15605  ruclem11  16177  4sqlem11  16895  vdwapf  16912  vdwlem11  16931  0ram  16960  funcres2b  17833  funcres2c  17839  setcepi  18024  yoniso  18220  isacs4lem  18479  chnso  18559  mgmhmima  18652  mhmima  18762  gsumwspan  18783  frmdss2  18800  cycsubm  19143  cycsubgcl  19147  cycsubgss  19148  ghmrn  19170  conjnmz  19193  ghmqusnsg  19223  ghmquskerlem3  19227  cntzmhm  19282  f1omvdconj  19387  odf1o2  19514  pgpssslw  19555  sylow2blem1  19561  lsmssv  19584  smndlsmidm  19597  pj1ghm2  19645  efgsp1  19678  efgrelexlemb  19691  cntzcmnf  19786  cyggenod  19825  gsumval3eu  19845  gsumval3lem2  19847  gsumval3  19848  gsumzsubmcl  19859  gsumzaddlem  19862  gsumzadd  19863  gsumzsplit  19868  gsumconst  19875  gsumzoppg  19885  gsumpt  19903  dmdprdd  19942  dprdfcntz  19958  dprdfeq0  19965  dprdlub  19969  dprdres  19971  dprdss  19972  dprdz  19973  subgdprd  19978  dprd2dlem1  19984  dprd2da  19985  dmdprdsplit2lem  19988  dpjghm2  20007  ablfac1b  20013  lmhmlsp  21013  pj1lmhm2  21065  pjfo  21682  frlmsplit2  21740  frlmsslsp  21763  frlmlbs  21764  frlmup3  21767  frlmup4  21768  lindff1  21787  lindfrn  21788  f1lindf  21789  indlcim  21807  aspval2  21866  mplcoe5lem  22006  mplbas2  22009  mplind  22037  evlslem1  22049  evlseu  22050  gsumply1subr  22186  m2cpmf1  22699  m2cpmghm  22700  iinopn  22858  pptbas  22964  tgrest  23115  resttopon  23117  rest0  23125  restfpw  23135  ordtbaslem  23144  ordtuni  23146  ordtbas2  23147  ordtrest  23158  ordtrest2  23160  cnclsi  23228  cnrest2r  23243  cnprest2  23246  lmss  23254  cncmp  23348  rncmp  23352  discmp  23354  connima  23381  conncn  23382  2ndcdisj  23412  2ndcomap  23414  dis2ndc  23416  lly1stc  23452  comppfsc  23488  kgencmp  23501  1stckgenlem  23509  kgencn3  23514  ptbasfi  23537  txbasval  23562  upxp  23579  uptx  23581  txtube  23596  txcmplem1  23597  txcmplem2  23598  tx1stc  23606  xkoptsub  23610  xkoco2cn  23614  xkococnlem  23615  hmeores  23727  fbasrn  23840  trfilss  23845  trfg  23847  uzrest  23853  rnelfmlem  23908  fclscmpi  23985  alexsublem  24000  ptcmplem1  24008  ptcmplem3  24010  cnextcn  24023  tmdgsum2  24052  subgtgp  24061  subgntr  24063  opnsubg  24064  clsnsg  24066  tgpconncomp  24069  tsmsfbas  24084  prdsdsf  24323  prdsxmetlem  24324  prdsmet  24326  imasdsf1olem  24329  unirnblps  24375  unirnbl  24376  prdsbl  24447  met1stc  24477  met2ndci  24478  prdsxmslem2  24485  xrge0gsumle  24790  xrge0tsms  24791  metdcn2  24796  metdsf  24805  metdsge  24806  cnmptre  24889  bndth  24925  evth  24926  evth2  24927  lebnumlem2  24929  lebnumlem3  24930  reparphti  24964  reparphtiOLD  24965  bcthlem5  25296  minveclem1  25392  minveclem3b  25396  evthicc2  25429  ovolmge0  25446  ovollb  25448  ovolgelb  25449  ovollb2lem  25457  ovollb2  25458  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliun  25474  ovoliun2  25475  ovolscalem1  25482  ovolicc1  25485  ovolicc2lem4  25489  ovolicc2  25491  voliunlem2  25520  voliunlem3  25521  ioombl1lem2  25528  ioombl1lem4  25530  uniioovol  25548  uniiccvol  25549  uniioombllem1  25550  uniioombllem2  25552  uniioombllem3  25554  uniioombllem6  25557  uniioombl  25558  volsup2  25574  vitalilem2  25578  vitalilem4  25580  vitalilem5  25581  mbfsup  25633  mbfinf  25634  mbflimsup  25635  i1fima  25647  i1fima2  25648  itg1cl  25654  itg1ge0  25655  i1fmullem  25663  i1fadd  25664  i1fmul  25665  itg1addlem4  25668  itg1addlem5  25669  i1fmulc  25672  itg1mulc  25673  i1fres  25674  itg10a  25679  itg1ge0a  25680  itg1climres  25683  mbfi1fseqlem4  25687  itg2seq  25711  itg2monolem1  25719  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  itg2i1fseq2  25725  itg2gt0  25729  itg2cnlem1  25730  itg2cn  25732  dvne0  25984  lhop2  25988  mdegleb  26037  mdegldg  26039  aalioulem3  26310  logccv  26640  efrlim  26947  efrlimOLD  26948  basellem3  27061  fsumvma  27192  lgseisenlem4  27357  noseqind  28300  uhgredgn0  29213  upgredgss  29217  umgredgss  29218  edgupgr  29219  upgredg  29222  usgruspgrb  29268  upgrres1  29398  ubthlem1  30958  minvecolem1  30962  htthlem  31005  ofrn  32729  ofrn2  32730  xppreima2  32741  fsumiunle  32921  ccatws1f1olast  33045  mgcf1o  33096  gsumhashmul  33161  xrge0tsmsd  33167  symgcom  33177  cycpmcl  33210  cycpmco2lem1  33220  cycpmco2lem5  33224  cycpmco2  33227  cycpmconjv  33236  cycpmconjslem2  33249  elrgspnsubrunlem2  33342  idomsubr  33403  1arithidom  33630  psrbasfsupp  33705  esplyfv  33747  esplyfval3  33749  ply1degltdimlem  33800  cmpcref  34028  ordtrestNEW  34099  ordtrest2NEW  34101  xrge0mulc1cn  34119  rge0scvg  34127  esumcst  34241  esumpfinvallem  34252  esumpcvgval  34256  esumiun  34272  omssubadd  34478  carsggect  34496  sibfinima  34517  sitgclg  34520  sitgaddlemb  34526  eulerpartgbij  34550  rrvrnss  34625  orvcval4  34639  erdsze2lem2  35420  cvxpconn  35458  cvxsconn  35459  cvmsss2  35490  cvmliftlem8  35508  cvmlift3lem6  35540  mrsubrn  35729  msubrn  35745  mvtss  35769  mclsssvlem  35778  mclsax  35785  mclsind  35786  neibastop2lem  36576  tailfb  36593  knoppcnlem10  36724  lindsdom  37865  poimirlem2  37873  poimirlem11  37882  poimirlem19  37890  poimirlem27  37898  poimirlem30  37901  mblfinlem2  37909  itg2addnclem2  37923  itg2gt0cn  37926  ftc1anclem3  37946  ftc1anclem6  37949  ftc1anclem7  37950  ftc1anc  37952  cnresima  38015  istotbnd3  38022  sstotbnd2  38025  totbndbnd  38040  prdsbnd  38044  cntotbnd  38047  ismtyima  38054  heibor1lem  38060  heibor  38072  rrnequiv  38086  lsatlss  39372  cdleme50rnlem  40920  sticksstones2  42517  aks6d1c6lem5  42547  cmpfiiin  43054  isnacs3  43067  eldioph2lem2  43118  fnwe2lem2  43408  lmhmfgima  43441  cantnfub2  43679  onnoxpg  43785  gneispacern  44494  imo72b2lem2  44523  imo72b2lem1  44525  imo72b2  44528  refsumcn  45390  cncmpmax  45392  elpmrn  45578  climinf  45966  climinf2lem  46064  limsupvaluz2  46096  supcnvlimsup  46098  limsupgtlem  46135  icccncfext  46245  dvsinax  46271  itgsubsticclem  46333  fourierdlem70  46534  fourierdlem82  46546  fge0npnf  46725  sge0resrnlem  46761  sge0isum  46785  sge0seq  46804  meadjiunlem  46823  omeiunle  46875  hoicvr  46906  vonvolmbllem  47018  preimaioomnf  47077  smfco  47160  chnsubseqwl  47237  ackvalsucsucval  49048  aacllem  50160