Theorem frnd 6671

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

Syntax hints:   → wi 4   ⊆ wss 3890  ran crn 5626  ⟶wf 6489

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 6497

This theorem is referenced by:  f1un  6795  fliftrel  7257  f1iun  7891  f1dmex  7904  fo2ndf  8065  onoviun  8277  onnseq  8278  smores2  8288  domdifsn  8992  omxpenlem  9010  fodomr  9060  domss2  9068  f1domfi  9109  sucdom2  9131  f1finf1o  9177  infn0  9206  f1fi  9218  fodomfir  9232  unirnffid  9251  intrnfi  9323  dffi3  9338  ordtypelem8  9434  ordtypelem9  9435  ordtypelem10  9436  hartogslem1  9451  brwdom2  9482  unxpwdom2  9497  ixpiunwdom  9499  infdifsn  9572  cantnf  9608  ac10ct  9950  numacn  9965  infpwfien  9978  fictb  10160  isf34lem5  10294  isf34lem7  10295  isf34lem6  10296  enfin1ai  10300  canthp1lem2  10570  gch3  10593  wuncval2  10664  peano5nni  12171  hashimarn  14396  hashf1lem1  14411  hashf1lem2  14412  ccatrn  14546  swrdrn  14609  pfxrn  14642  cshwrn  14758  limsupgle  15433  limsupgre  15437  isercolllem2  15622  isercoll  15624  isercoll2  15625  climsup  15626  ruclem11  16201  4sqlem11  16920  vdwapf  16937  vdwlem11  16956  0ram  16985  funcres2b  17858  funcres2c  17864  setcepi  18049  yoniso  18245  isacs4lem  18504  chnso  18584  mgmhmima  18677  mhmima  18787  gsumwspan  18808  frmdss2  18825  cycsubm  19171  cycsubgcl  19175  cycsubgss  19176  ghmrn  19198  conjnmz  19221  ghmqusnsg  19251  ghmquskerlem3  19255  cntzmhm  19310  f1omvdconj  19415  odf1o2  19542  pgpssslw  19583  sylow2blem1  19589  lsmssv  19612  smndlsmidm  19625  pj1ghm2  19673  efgsp1  19706  efgrelexlemb  19719  cntzcmnf  19814  cyggenod  19853  gsumval3eu  19873  gsumval3lem2  19875  gsumval3  19876  gsumzsubmcl  19887  gsumzaddlem  19890  gsumzadd  19891  gsumzsplit  19896  gsumconst  19903  gsumzoppg  19913  gsumpt  19931  dmdprdd  19970  dprdfcntz  19986  dprdfeq0  19993  dprdlub  19997  dprdres  19999  dprdss  20000  dprdz  20001  subgdprd  20006  dprd2dlem1  20012  dprd2da  20013  dmdprdsplit2lem  20016  dpjghm2  20035  ablfac1b  20041  lmhmlsp  21039  pj1lmhm2  21091  pjfo  21708  frlmsplit2  21766  frlmsslsp  21789  frlmlbs  21790  frlmup3  21793  frlmup4  21794  lindff1  21813  lindfrn  21814  f1lindf  21815  indlcim  21833  aspval2  21891  mplcoe5lem  22030  mplbas2  22033  mplind  22061  evlslem1  22073  evlseu  22074  gsumply1subr  22210  m2cpmf1  22721  m2cpmghm  22722  iinopn  22880  pptbas  22986  tgrest  23137  resttopon  23139  rest0  23147  restfpw  23157  ordtbaslem  23166  ordtuni  23168  ordtbas2  23169  ordtrest  23180  ordtrest2  23182  cnclsi  23250  cnrest2r  23265  cnprest2  23268  lmss  23276  cncmp  23370  rncmp  23374  discmp  23376  connima  23403  conncn  23404  2ndcdisj  23434  2ndcomap  23436  dis2ndc  23438  lly1stc  23474  comppfsc  23510  kgencmp  23523  1stckgenlem  23531  kgencn3  23536  ptbasfi  23559  txbasval  23584  upxp  23601  uptx  23603  txtube  23618  txcmplem1  23619  txcmplem2  23620  tx1stc  23628  xkoptsub  23632  xkoco2cn  23636  xkococnlem  23637  hmeores  23749  fbasrn  23862  trfilss  23867  trfg  23869  uzrest  23875  rnelfmlem  23930  fclscmpi  24007  alexsublem  24022  ptcmplem1  24030  ptcmplem3  24032  cnextcn  24045  tmdgsum2  24074  subgtgp  24083  subgntr  24085  opnsubg  24086  clsnsg  24088  tgpconncomp  24091  tsmsfbas  24106  prdsdsf  24345  prdsxmetlem  24346  prdsmet  24348  imasdsf1olem  24351  unirnblps  24397  unirnbl  24398  prdsbl  24469  met1stc  24499  met2ndci  24500  prdsxmslem2  24507  xrge0gsumle  24812  xrge0tsms  24813  metdcn2  24818  metdsf  24827  metdsge  24828  cnmptre  24907  bndth  24938  evth  24939  evth2  24940  lebnumlem2  24942  lebnumlem3  24943  reparphti  24977  bcthlem5  25308  minveclem1  25404  minveclem3b  25408  evthicc2  25440  ovolmge0  25457  ovollb  25459  ovolgelb  25460  ovollb2lem  25468  ovollb2  25469  ovolunlem1a  25476  ovolunlem1  25477  ovoliunlem1  25482  ovoliun  25485  ovoliun2  25486  ovolscalem1  25493  ovolicc1  25496  ovolicc2lem4  25500  ovolicc2  25502  voliunlem2  25531  voliunlem3  25532  ioombl1lem2  25539  ioombl1lem4  25541  uniioovol  25559  uniiccvol  25560  uniioombllem1  25561  uniioombllem2  25563  uniioombllem3  25565  uniioombllem6  25568  uniioombl  25569  volsup2  25585  vitalilem2  25589  vitalilem4  25591  vitalilem5  25592  mbfsup  25644  mbfinf  25645  mbflimsup  25646  i1fima  25658  i1fima2  25659  itg1cl  25665  itg1ge0  25666  i1fmullem  25674  i1fadd  25675  i1fmul  25676  itg1addlem4  25679  itg1addlem5  25680  i1fmulc  25683  itg1mulc  25684  i1fres  25685  itg10a  25690  itg1ge0a  25691  itg1climres  25694  mbfi1fseqlem4  25698  itg2seq  25722  itg2monolem1  25730  itg2monolem2  25731  itg2monolem3  25732  itg2mono  25733  itg2i1fseq2  25736  itg2gt0  25740  itg2cnlem1  25741  itg2cn  25743  dvne0  25991  lhop2  25995  mdegleb  26042  mdegldg  26044  aalioulem3  26314  logccv  26643  efrlim  26949  efrlimOLD  26950  basellem3  27063  fsumvma  27193  lgseisenlem4  27358  noseqind  28301  uhgredgn0  29214  upgredgss  29218  umgredgss  29219  edgupgr  29220  upgredg  29223  usgruspgrb  29269  upgrres1  29399  ubthlem1  30959  minvecolem1  30963  htthlem  31006  ofrn  32730  ofrn2  32731  xppreima2  32742  fsumiunle  32920  ccatws1f1olast  33030  mgcf1o  33081  gsumhashmul  33146  xrge0tsmsd  33152  symgcom  33162  cycpmcl  33195  cycpmco2lem1  33205  cycpmco2lem5  33209  cycpmco2  33212  cycpmconjv  33221  cycpmconjslem2  33234  elrgspnsubrunlem2  33327  idomsubr  33388  1arithidom  33615  psrbasfsupp  33690  esplyfv  33732  esplyfval3  33734  ply1degltdimlem  33785  cmpcref  34013  ordtrestNEW  34084  ordtrest2NEW  34086  xrge0mulc1cn  34104  rge0scvg  34112  esumcst  34226  esumpfinvallem  34237  esumpcvgval  34241  esumiun  34257  omssubadd  34463  carsggect  34481  sibfinima  34502  sitgclg  34505  sitgaddlemb  34511  eulerpartgbij  34535  rrvrnss  34610  orvcval4  34624  erdsze2lem2  35405  cvxpconn  35443  cvxsconn  35444  cvmsss2  35475  cvmliftlem8  35493  cvmlift3lem6  35525  mrsubrn  35714  msubrn  35730  mvtss  35754  mclsssvlem  35763  mclsax  35770  mclsind  35771  neibastop2lem  36561  tailfb  36578  knoppcnlem10  36781  lindsdom  37952  poimirlem2  37960  poimirlem11  37969  poimirlem19  37977  poimirlem27  37985  poimirlem30  37988  mblfinlem2  37996  itg2addnclem2  38010  itg2gt0cn  38013  ftc1anclem3  38033  ftc1anclem6  38036  ftc1anclem7  38037  ftc1anc  38039  cnresima  38102  istotbnd3  38109  sstotbnd2  38112  totbndbnd  38127  prdsbnd  38131  cntotbnd  38134  ismtyima  38141  heibor1lem  38147  heibor  38159  rrnequiv  38173  lsatlss  39459  cdleme50rnlem  41007  sticksstones2  42603  aks6d1c6lem5  42633  cmpfiiin  43146  isnacs3  43159  eldioph2lem2  43210  fnwe2lem2  43500  lmhmfgima  43533  cantnfub2  43771  onnoxpg  43877  gneispacern  44586  imo72b2lem2  44615  imo72b2lem1  44617  imo72b2  44620  refsumcn  45482  cncmpmax  45484  elpmrn  45670  climinf  46057  climinf2lem  46155  limsupvaluz2  46187  supcnvlimsup  46189  limsupgtlem  46226  icccncfext  46336  dvsinax  46362  itgsubsticclem  46424  fourierdlem70  46625  fourierdlem82  46637  fge0npnf  46816  sge0resrnlem  46852  sge0isum  46876  sge0seq  46895  meadjiunlem  46914  omeiunle  46966  hoicvr  46997  vonvolmbllem  47109  preimaioomnf  47168  smfco  47251  chnsubseqwl  47328  ackvalsucsucval  49179  aacllem  50291