Theorem frnd 6670

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

Syntax hints:   → wi 4   ⊆ wss 3901  ran crn 5625  ⟶wf 6488

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 6496

This theorem is referenced by:  f1un  6794  fliftrel  7254  f1iun  7888  f1dmex  7901  fo2ndf  8063  onoviun  8275  onnseq  8276  smores2  8286  domdifsn  8988  omxpenlem  9006  fodomr  9056  domss2  9064  f1domfi  9105  sucdom2  9127  f1finf1o  9173  infn0  9202  f1fi  9214  fodomfir  9228  unirnffid  9247  intrnfi  9319  dffi3  9334  ordtypelem8  9430  ordtypelem9  9431  ordtypelem10  9432  hartogslem1  9447  brwdom2  9478  unxpwdom2  9493  ixpiunwdom  9495  infdifsn  9566  cantnf  9602  ac10ct  9944  numacn  9959  infpwfien  9972  fictb  10154  isf34lem5  10288  isf34lem7  10289  isf34lem6  10290  enfin1ai  10294  canthp1lem2  10564  gch3  10587  wuncval2  10658  peano5nni  12148  hashimarn  14363  hashf1lem1  14378  hashf1lem2  14379  ccatrn  14513  swrdrn  14576  pfxrn  14609  cshwrn  14725  limsupgle  15400  limsupgre  15404  isercolllem2  15589  isercoll  15591  isercoll2  15592  climsup  15593  ruclem11  16165  4sqlem11  16883  vdwapf  16900  vdwlem11  16919  0ram  16948  funcres2b  17821  funcres2c  17827  setcepi  18012  yoniso  18208  isacs4lem  18467  chnso  18547  mgmhmima  18640  mhmima  18750  gsumwspan  18771  frmdss2  18788  cycsubm  19131  cycsubgcl  19135  cycsubgss  19136  ghmrn  19158  conjnmz  19181  ghmqusnsg  19211  ghmquskerlem3  19215  cntzmhm  19270  f1omvdconj  19375  odf1o2  19502  pgpssslw  19543  sylow2blem1  19549  lsmssv  19572  smndlsmidm  19585  pj1ghm2  19633  efgsp1  19666  efgrelexlemb  19679  cntzcmnf  19774  cyggenod  19813  gsumval3eu  19833  gsumval3lem2  19835  gsumval3  19836  gsumzsubmcl  19847  gsumzaddlem  19850  gsumzadd  19851  gsumzsplit  19856  gsumconst  19863  gsumzoppg  19873  gsumpt  19891  dmdprdd  19930  dprdfcntz  19946  dprdfeq0  19953  dprdlub  19957  dprdres  19959  dprdss  19960  dprdz  19961  subgdprd  19966  dprd2dlem1  19972  dprd2da  19973  dmdprdsplit2lem  19976  dpjghm2  19995  ablfac1b  20001  lmhmlsp  21001  pj1lmhm2  21053  pjfo  21670  frlmsplit2  21728  frlmsslsp  21751  frlmlbs  21752  frlmup3  21755  frlmup4  21756  lindff1  21775  lindfrn  21776  f1lindf  21777  indlcim  21795  aspval2  21854  mplcoe5lem  21994  mplbas2  21997  mplind  22025  evlslem1  22037  evlseu  22038  gsumply1subr  22174  m2cpmf1  22687  m2cpmghm  22688  iinopn  22846  pptbas  22952  tgrest  23103  resttopon  23105  rest0  23113  restfpw  23123  ordtbaslem  23132  ordtuni  23134  ordtbas2  23135  ordtrest  23146  ordtrest2  23148  cnclsi  23216  cnrest2r  23231  cnprest2  23234  lmss  23242  cncmp  23336  rncmp  23340  discmp  23342  connima  23369  conncn  23370  2ndcdisj  23400  2ndcomap  23402  dis2ndc  23404  lly1stc  23440  comppfsc  23476  kgencmp  23489  1stckgenlem  23497  kgencn3  23502  ptbasfi  23525  txbasval  23550  upxp  23567  uptx  23569  txtube  23584  txcmplem1  23585  txcmplem2  23586  tx1stc  23594  xkoptsub  23598  xkoco2cn  23602  xkococnlem  23603  hmeores  23715  fbasrn  23828  trfilss  23833  trfg  23835  uzrest  23841  rnelfmlem  23896  fclscmpi  23973  alexsublem  23988  ptcmplem1  23996  ptcmplem3  23998  cnextcn  24011  tmdgsum2  24040  subgtgp  24049  subgntr  24051  opnsubg  24052  clsnsg  24054  tgpconncomp  24057  tsmsfbas  24072  prdsdsf  24311  prdsxmetlem  24312  prdsmet  24314  imasdsf1olem  24317  unirnblps  24363  unirnbl  24364  prdsbl  24435  met1stc  24465  met2ndci  24466  prdsxmslem2  24473  xrge0gsumle  24778  xrge0tsms  24779  metdcn2  24784  metdsf  24793  metdsge  24794  cnmptre  24877  bndth  24913  evth  24914  evth2  24915  lebnumlem2  24917  lebnumlem3  24918  reparphti  24952  reparphtiOLD  24953  bcthlem5  25284  minveclem1  25380  minveclem3b  25384  evthicc2  25417  ovolmge0  25434  ovollb  25436  ovolgelb  25437  ovollb2lem  25445  ovollb2  25446  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliun  25462  ovoliun2  25463  ovolscalem1  25470  ovolicc1  25473  ovolicc2lem4  25477  ovolicc2  25479  voliunlem2  25508  voliunlem3  25509  ioombl1lem2  25516  ioombl1lem4  25518  uniioovol  25536  uniiccvol  25537  uniioombllem1  25538  uniioombllem2  25540  uniioombllem3  25542  uniioombllem6  25545  uniioombl  25546  volsup2  25562  vitalilem2  25566  vitalilem4  25568  vitalilem5  25569  mbfsup  25621  mbfinf  25622  mbflimsup  25623  i1fima  25635  i1fima2  25636  itg1cl  25642  itg1ge0  25643  i1fmullem  25651  i1fadd  25652  i1fmul  25653  itg1addlem4  25656  itg1addlem5  25657  i1fmulc  25660  itg1mulc  25661  i1fres  25662  itg10a  25667  itg1ge0a  25668  itg1climres  25671  mbfi1fseqlem4  25675  itg2seq  25699  itg2monolem1  25707  itg2monolem2  25708  itg2monolem3  25709  itg2mono  25710  itg2i1fseq2  25713  itg2gt0  25717  itg2cnlem1  25718  itg2cn  25720  dvne0  25972  lhop2  25976  mdegleb  26025  mdegldg  26027  aalioulem3  26298  logccv  26628  efrlim  26935  efrlimOLD  26936  basellem3  27049  fsumvma  27180  lgseisenlem4  27345  noseqind  28288  uhgredgn0  29201  upgredgss  29205  umgredgss  29206  edgupgr  29207  upgredg  29210  usgruspgrb  29256  upgrres1  29386  ubthlem1  30945  minvecolem1  30949  htthlem  30992  ofrn  32717  ofrn2  32718  xppreima2  32729  fsumiunle  32910  ccatws1f1olast  33034  mgcf1o  33085  gsumhashmul  33150  xrge0tsmsd  33155  symgcom  33165  cycpmcl  33198  cycpmco2lem1  33208  cycpmco2lem5  33212  cycpmco2  33215  cycpmconjv  33224  cycpmconjslem2  33237  elrgspnsubrunlem2  33330  idomsubr  33391  1arithidom  33618  psrbasfsupp  33693  esplyfv  33728  esplyfval3  33730  ply1degltdimlem  33779  cmpcref  34007  ordtrestNEW  34078  ordtrest2NEW  34080  xrge0mulc1cn  34098  rge0scvg  34106  esumcst  34220  esumpfinvallem  34231  esumpcvgval  34235  esumiun  34251  omssubadd  34457  carsggect  34475  sibfinima  34496  sitgclg  34499  sitgaddlemb  34505  eulerpartgbij  34529  rrvrnss  34604  orvcval4  34618  erdsze2lem2  35398  cvxpconn  35436  cvxsconn  35437  cvmsss2  35468  cvmliftlem8  35486  cvmlift3lem6  35518  mrsubrn  35707  msubrn  35723  mvtss  35747  mclsssvlem  35756  mclsax  35763  mclsind  35764  neibastop2lem  36554  tailfb  36571  knoppcnlem10  36702  lindsdom  37815  poimirlem2  37823  poimirlem11  37832  poimirlem19  37840  poimirlem27  37848  poimirlem30  37851  mblfinlem2  37859  itg2addnclem2  37873  itg2gt0cn  37876  ftc1anclem3  37896  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anc  37902  cnresima  37965  istotbnd3  37972  sstotbnd2  37975  totbndbnd  37990  prdsbnd  37994  cntotbnd  37997  ismtyima  38004  heibor1lem  38010  heibor  38022  rrnequiv  38036  lsatlss  39266  cdleme50rnlem  40814  sticksstones2  42411  aks6d1c6lem5  42441  cmpfiiin  42949  isnacs3  42962  eldioph2lem2  43013  fnwe2lem2  43303  lmhmfgima  43336  cantnfub2  43574  onnoxpg  43680  gneispacern  44389  imo72b2lem2  44418  imo72b2lem1  44420  imo72b2  44423  refsumcn  45285  cncmpmax  45287  elpmrn  45474  climinf  45862  climinf2lem  45960  limsupvaluz2  45992  supcnvlimsup  45994  limsupgtlem  46031  icccncfext  46141  dvsinax  46167  itgsubsticclem  46229  fourierdlem70  46430  fourierdlem82  46442  fge0npnf  46621  sge0resrnlem  46657  sge0isum  46681  sge0seq  46700  meadjiunlem  46719  omeiunle  46771  hoicvr  46802  vonvolmbllem  46914  preimaioomnf  46973  smfco  47056  chnsubseqwl  47133  ackvalsucsucval  48944  aacllem  50056