Theorem frnd 6668

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

Syntax hints:   → wi 4   ⊆ wss 3899  ran crn 5623  ⟶wf 6486

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 6494

This theorem is referenced by:  f1un  6792  fliftrel  7252  f1iun  7886  f1dmex  7899  fo2ndf  8061  onoviun  8273  onnseq  8274  smores2  8284  domdifsn  8986  omxpenlem  9004  fodomr  9054  domss2  9062  f1domfi  9103  sucdom2  9125  f1finf1o  9171  infn0  9200  f1fi  9212  fodomfir  9226  unirnffid  9245  intrnfi  9317  dffi3  9332  ordtypelem8  9428  ordtypelem9  9429  ordtypelem10  9430  hartogslem1  9445  brwdom2  9476  unxpwdom2  9491  ixpiunwdom  9493  infdifsn  9564  cantnf  9600  ac10ct  9942  numacn  9957  infpwfien  9970  fictb  10152  isf34lem5  10286  isf34lem7  10287  isf34lem6  10288  enfin1ai  10292  canthp1lem2  10562  gch3  10585  wuncval2  10656  peano5nni  12146  hashimarn  14361  hashf1lem1  14376  hashf1lem2  14377  ccatrn  14511  swrdrn  14574  pfxrn  14607  cshwrn  14723  limsupgle  15398  limsupgre  15402  isercolllem2  15587  isercoll  15589  isercoll2  15590  climsup  15591  ruclem11  16163  4sqlem11  16881  vdwapf  16898  vdwlem11  16917  0ram  16946  funcres2b  17819  funcres2c  17825  setcepi  18010  yoniso  18206  isacs4lem  18465  chnso  18545  mgmhmima  18638  mhmima  18748  gsumwspan  18769  frmdss2  18786  cycsubm  19129  cycsubgcl  19133  cycsubgss  19134  ghmrn  19156  conjnmz  19179  ghmqusnsg  19209  ghmquskerlem3  19213  cntzmhm  19268  f1omvdconj  19373  odf1o2  19500  pgpssslw  19541  sylow2blem1  19547  lsmssv  19570  smndlsmidm  19583  pj1ghm2  19631  efgsp1  19664  efgrelexlemb  19677  cntzcmnf  19772  cyggenod  19811  gsumval3eu  19831  gsumval3lem2  19833  gsumval3  19834  gsumzsubmcl  19845  gsumzaddlem  19848  gsumzadd  19849  gsumzsplit  19854  gsumconst  19861  gsumzoppg  19871  gsumpt  19889  dmdprdd  19928  dprdfcntz  19944  dprdfeq0  19951  dprdlub  19955  dprdres  19957  dprdss  19958  dprdz  19959  subgdprd  19964  dprd2dlem1  19970  dprd2da  19971  dmdprdsplit2lem  19974  dpjghm2  19993  ablfac1b  19999  lmhmlsp  20999  pj1lmhm2  21051  pjfo  21668  frlmsplit2  21726  frlmsslsp  21749  frlmlbs  21750  frlmup3  21753  frlmup4  21754  lindff1  21773  lindfrn  21774  f1lindf  21775  indlcim  21793  aspval2  21852  mplcoe5lem  21992  mplbas2  21995  mplind  22023  evlslem1  22035  evlseu  22036  gsumply1subr  22172  m2cpmf1  22685  m2cpmghm  22686  iinopn  22844  pptbas  22950  tgrest  23101  resttopon  23103  rest0  23111  restfpw  23121  ordtbaslem  23130  ordtuni  23132  ordtbas2  23133  ordtrest  23144  ordtrest2  23146  cnclsi  23214  cnrest2r  23229  cnprest2  23232  lmss  23240  cncmp  23334  rncmp  23338  discmp  23340  connima  23367  conncn  23368  2ndcdisj  23398  2ndcomap  23400  dis2ndc  23402  lly1stc  23438  comppfsc  23474  kgencmp  23487  1stckgenlem  23495  kgencn3  23500  ptbasfi  23523  txbasval  23548  upxp  23565  uptx  23567  txtube  23582  txcmplem1  23583  txcmplem2  23584  tx1stc  23592  xkoptsub  23596  xkoco2cn  23600  xkococnlem  23601  hmeores  23713  fbasrn  23826  trfilss  23831  trfg  23833  uzrest  23839  rnelfmlem  23894  fclscmpi  23971  alexsublem  23986  ptcmplem1  23994  ptcmplem3  23996  cnextcn  24009  tmdgsum2  24038  subgtgp  24047  subgntr  24049  opnsubg  24050  clsnsg  24052  tgpconncomp  24055  tsmsfbas  24070  prdsdsf  24309  prdsxmetlem  24310  prdsmet  24312  imasdsf1olem  24315  unirnblps  24361  unirnbl  24362  prdsbl  24433  met1stc  24463  met2ndci  24464  prdsxmslem2  24471  xrge0gsumle  24776  xrge0tsms  24777  metdcn2  24782  metdsf  24791  metdsge  24792  cnmptre  24875  bndth  24911  evth  24912  evth2  24913  lebnumlem2  24915  lebnumlem3  24916  reparphti  24950  reparphtiOLD  24951  bcthlem5  25282  minveclem1  25378  minveclem3b  25382  evthicc2  25415  ovolmge0  25432  ovollb  25434  ovolgelb  25435  ovollb2lem  25443  ovollb2  25444  ovolunlem1a  25451  ovolunlem1  25452  ovoliunlem1  25457  ovoliun  25460  ovoliun2  25461  ovolscalem1  25468  ovolicc1  25471  ovolicc2lem4  25475  ovolicc2  25477  voliunlem2  25506  voliunlem3  25507  ioombl1lem2  25514  ioombl1lem4  25516  uniioovol  25534  uniiccvol  25535  uniioombllem1  25536  uniioombllem2  25538  uniioombllem3  25540  uniioombllem6  25543  uniioombl  25544  volsup2  25560  vitalilem2  25564  vitalilem4  25566  vitalilem5  25567  mbfsup  25619  mbfinf  25620  mbflimsup  25621  i1fima  25633  i1fima2  25634  itg1cl  25640  itg1ge0  25641  i1fmullem  25649  i1fadd  25650  i1fmul  25651  itg1addlem4  25654  itg1addlem5  25655  i1fmulc  25658  itg1mulc  25659  i1fres  25660  itg10a  25665  itg1ge0a  25666  itg1climres  25669  mbfi1fseqlem4  25673  itg2seq  25697  itg2monolem1  25705  itg2monolem2  25706  itg2monolem3  25707  itg2mono  25708  itg2i1fseq2  25711  itg2gt0  25715  itg2cnlem1  25716  itg2cn  25718  dvne0  25970  lhop2  25974  mdegleb  26023  mdegldg  26025  aalioulem3  26296  logccv  26626  efrlim  26933  efrlimOLD  26934  basellem3  27047  fsumvma  27178  lgseisenlem4  27343  noseqind  28253  uhgredgn0  29150  upgredgss  29154  umgredgss  29155  edgupgr  29156  upgredg  29159  usgruspgrb  29205  upgrres1  29335  ubthlem1  30894  minvecolem1  30898  htthlem  30941  ofrn  32666  ofrn2  32667  xppreima2  32678  fsumiunle  32859  ccatws1f1olast  32983  mgcf1o  33034  gsumhashmul  33099  xrge0tsmsd  33104  symgcom  33114  cycpmcl  33147  cycpmco2lem1  33157  cycpmco2lem5  33161  cycpmco2  33164  cycpmconjv  33173  cycpmconjslem2  33186  elrgspnsubrunlem2  33279  idomsubr  33340  1arithidom  33567  psrbasfsupp  33642  esplyfv  33677  esplyfval3  33679  ply1degltdimlem  33728  cmpcref  33956  ordtrestNEW  34027  ordtrest2NEW  34029  xrge0mulc1cn  34047  rge0scvg  34055  esumcst  34169  esumpfinvallem  34180  esumpcvgval  34184  esumiun  34200  omssubadd  34406  carsggect  34424  sibfinima  34445  sitgclg  34448  sitgaddlemb  34454  eulerpartgbij  34478  rrvrnss  34553  orvcval4  34567  erdsze2lem2  35347  cvxpconn  35385  cvxsconn  35386  cvmsss2  35417  cvmliftlem8  35435  cvmlift3lem6  35467  mrsubrn  35656  msubrn  35672  mvtss  35696  mclsssvlem  35705  mclsax  35712  mclsind  35713  neibastop2lem  36503  tailfb  36520  knoppcnlem10  36645  lindsdom  37754  poimirlem2  37762  poimirlem11  37771  poimirlem19  37779  poimirlem27  37787  poimirlem30  37790  mblfinlem2  37798  itg2addnclem2  37812  itg2gt0cn  37815  ftc1anclem3  37835  ftc1anclem6  37838  ftc1anclem7  37839  ftc1anc  37841  cnresima  37904  istotbnd3  37911  sstotbnd2  37914  totbndbnd  37929  prdsbnd  37933  cntotbnd  37936  ismtyima  37943  heibor1lem  37949  heibor  37961  rrnequiv  37975  lsatlss  39195  cdleme50rnlem  40743  sticksstones2  42340  aks6d1c6lem5  42370  cmpfiiin  42881  isnacs3  42894  eldioph2lem2  42945  fnwe2lem2  43235  lmhmfgima  43268  cantnfub2  43506  onnog  43612  gneispacern  44321  imo72b2lem2  44350  imo72b2lem1  44352  imo72b2  44355  refsumcn  45217  cncmpmax  45219  elpmrn  45406  climinf  45794  climinf2lem  45892  limsupvaluz2  45924  supcnvlimsup  45926  limsupgtlem  45963  icccncfext  46073  dvsinax  46099  itgsubsticclem  46161  fourierdlem70  46362  fourierdlem82  46374  fge0npnf  46553  sge0resrnlem  46589  sge0isum  46613  sge0seq  46632  meadjiunlem  46651  omeiunle  46703  hoicvr  46734  vonvolmbllem  46846  preimaioomnf  46905  smfco  46988  chnsubseqwl  47065  ackvalsucsucval  48876  aacllem  49988