Theorem frnd 6713

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

Syntax hints:   → wi 4   ⊆ wss 3926  ran crn 5655  ⟶wf 6526

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 6534

This theorem is referenced by:  f1un  6837  fliftrel  7300  f1iun  7940  f1dmex  7953  fo2ndf  8118  onoviun  8355  onnseq  8356  smores2  8366  domdifsn  9066  omxpenlem  9085  sucdom2OLD  9094  fodomr  9140  domss2  9148  f1domfi  9193  sucdom2  9215  f1finf1o  9275  f1finf1oOLD  9276  infn0  9310  f1fi  9322  fodomfir  9338  unirnffid  9357  intrnfi  9426  dffi3  9441  ordtypelem8  9537  ordtypelem9  9538  ordtypelem10  9539  hartogslem1  9554  brwdom2  9585  unxpwdom2  9600  ixpiunwdom  9602  infdifsn  9669  cantnf  9705  ac10ct  10046  numacn  10061  infpwfien  10074  fictb  10256  isf34lem5  10390  isf34lem7  10391  isf34lem6  10392  enfin1ai  10396  canthp1lem2  10665  gch3  10688  wuncval2  10759  peano5nni  12241  hashimarn  14456  hashf1lem1  14471  hashf1lem2  14472  ccatrn  14605  swrdrn  14668  pfxrn  14701  cshwrn  14818  limsupgle  15491  limsupgre  15495  isercolllem2  15680  isercoll  15682  isercoll2  15683  climsup  15684  ruclem11  16256  4sqlem11  16973  vdwapf  16990  vdwlem11  17009  0ram  17038  funcres2b  17908  funcres2c  17914  setcepi  18099  yoniso  18295  isacs4lem  18552  mgmhmima  18691  mhmima  18801  gsumwspan  18822  frmdss2  18839  cycsubm  19183  cycsubgcl  19187  cycsubgss  19188  ghmrn  19210  conjnmz  19233  ghmqusnsg  19263  ghmquskerlem3  19267  cntzmhm  19322  f1omvdconj  19425  odf1o2  19552  pgpssslw  19593  sylow2blem1  19599  lsmssv  19622  smndlsmidm  19635  pj1ghm2  19683  efgsp1  19716  efgrelexlemb  19729  cntzcmnf  19824  cyggenod  19863  gsumval3eu  19883  gsumval3lem2  19885  gsumval3  19886  gsumzsubmcl  19897  gsumzaddlem  19900  gsumzadd  19901  gsumzsplit  19906  gsumconst  19913  gsumzoppg  19923  gsumpt  19941  dmdprdd  19980  dprdfcntz  19996  dprdfeq0  20003  dprdlub  20007  dprdres  20009  dprdss  20010  dprdz  20011  subgdprd  20016  dprd2dlem1  20022  dprd2da  20023  dmdprdsplit2lem  20026  dpjghm2  20045  ablfac1b  20051  lmhmlsp  21005  pj1lmhm2  21057  pjfo  21673  frlmsplit2  21731  frlmsslsp  21754  frlmlbs  21755  frlmup3  21758  frlmup4  21759  lindff1  21778  lindfrn  21779  f1lindf  21780  indlcim  21798  aspval2  21856  mplcoe5lem  21995  mplbas2  21998  mplind  22026  evlslem1  22038  evlseu  22039  gsumply1subr  22167  m2cpmf1  22679  m2cpmghm  22680  iinopn  22838  pptbas  22944  tgrest  23095  resttopon  23097  rest0  23105  restfpw  23115  ordtbaslem  23124  ordtuni  23126  ordtbas2  23127  ordtrest  23138  ordtrest2  23140  cnclsi  23208  cnrest2r  23223  cnprest2  23226  lmss  23234  cncmp  23328  rncmp  23332  discmp  23334  connima  23361  conncn  23362  2ndcdisj  23392  2ndcomap  23394  dis2ndc  23396  lly1stc  23432  comppfsc  23468  kgencmp  23481  1stckgenlem  23489  kgencn3  23494  ptbasfi  23517  txbasval  23542  upxp  23559  uptx  23561  txtube  23576  txcmplem1  23577  txcmplem2  23578  tx1stc  23586  xkoptsub  23590  xkoco2cn  23594  xkococnlem  23595  hmeores  23707  fbasrn  23820  trfilss  23825  trfg  23827  uzrest  23833  rnelfmlem  23888  fclscmpi  23965  alexsublem  23980  ptcmplem1  23988  ptcmplem3  23990  cnextcn  24003  tmdgsum2  24032  subgtgp  24041  subgntr  24043  opnsubg  24044  clsnsg  24046  tgpconncomp  24049  tsmsfbas  24064  prdsdsf  24304  prdsxmetlem  24305  prdsmet  24307  imasdsf1olem  24310  unirnblps  24356  unirnbl  24357  prdsbl  24428  met1stc  24458  met2ndci  24459  prdsxmslem2  24466  xrge0gsumle  24771  xrge0tsms  24772  metdcn2  24777  metdsf  24786  metdsge  24787  cnmptre  24870  bndth  24906  evth  24907  evth2  24908  lebnumlem2  24910  lebnumlem3  24911  reparphti  24945  reparphtiOLD  24946  bcthlem5  25278  minveclem1  25374  minveclem3b  25378  evthicc2  25411  ovolmge0  25428  ovollb  25430  ovolgelb  25431  ovollb2lem  25439  ovollb2  25440  ovolunlem1a  25447  ovolunlem1  25448  ovoliunlem1  25453  ovoliun  25456  ovoliun2  25457  ovolscalem1  25464  ovolicc1  25467  ovolicc2lem4  25471  ovolicc2  25473  voliunlem2  25502  voliunlem3  25503  ioombl1lem2  25510  ioombl1lem4  25512  uniioovol  25530  uniiccvol  25531  uniioombllem1  25532  uniioombllem2  25534  uniioombllem3  25536  uniioombllem6  25539  uniioombl  25540  volsup2  25556  vitalilem2  25560  vitalilem4  25562  vitalilem5  25563  mbfsup  25615  mbfinf  25616  mbflimsup  25617  i1fima  25629  i1fima2  25630  itg1cl  25636  itg1ge0  25637  i1fmullem  25645  i1fadd  25646  i1fmul  25647  itg1addlem4  25650  itg1addlem5  25651  i1fmulc  25654  itg1mulc  25655  i1fres  25656  itg10a  25661  itg1ge0a  25662  itg1climres  25665  mbfi1fseqlem4  25669  itg2seq  25693  itg2monolem1  25701  itg2monolem2  25702  itg2monolem3  25703  itg2mono  25704  itg2i1fseq2  25707  itg2gt0  25711  itg2cnlem1  25712  itg2cn  25714  dvne0  25966  lhop2  25970  mdegleb  26019  mdegldg  26021  aalioulem3  26292  logccv  26622  efrlim  26929  efrlimOLD  26930  basellem3  27043  fsumvma  27174  lgseisenlem4  27339  noseqind  28215  uhgredgn0  29053  upgredgss  29057  umgredgss  29058  edgupgr  29059  upgredg  29062  usgruspgrb  29108  upgrres1  29238  ubthlem1  30797  minvecolem1  30801  htthlem  30844  ofrn  32563  ofrn2  32564  xppreima2  32575  fsumiunle  32754  ccatws1f1olast  32874  mgcf1o  32929  chnso  32940  gsumhashmul  33001  xrge0tsmsd  33002  symgcom  33040  cycpmcl  33073  cycpmco2lem1  33083  cycpmco2lem5  33087  cycpmco2  33090  cycpmconjv  33099  cycpmconjslem2  33112  elrgspnsubrunlem2  33189  idomsubr  33249  1arithidom  33498  ply1degltdimlem  33608  cmpcref  33827  ordtrestNEW  33898  ordtrest2NEW  33900  xrge0mulc1cn  33918  rge0scvg  33926  esumcst  34040  esumpfinvallem  34051  esumpcvgval  34055  esumiun  34071  omssubadd  34278  carsggect  34296  sibfinima  34317  sitgclg  34320  sitgaddlemb  34326  eulerpartgbij  34350  rrvrnss  34425  orvcval4  34439  erdsze2lem2  35172  cvxpconn  35210  cvxsconn  35211  cvmsss2  35242  cvmliftlem8  35260  cvmlift3lem6  35292  mrsubrn  35481  msubrn  35497  mvtss  35521  mclsssvlem  35530  mclsax  35537  mclsind  35538  neibastop2lem  36324  tailfb  36341  knoppcnlem10  36466  lindsdom  37584  poimirlem2  37592  poimirlem11  37601  poimirlem19  37609  poimirlem27  37617  poimirlem30  37620  mblfinlem2  37628  itg2addnclem2  37642  itg2gt0cn  37645  ftc1anclem3  37665  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anc  37671  cnresima  37734  istotbnd3  37741  sstotbnd2  37744  totbndbnd  37759  prdsbnd  37763  cntotbnd  37766  ismtyima  37773  heibor1lem  37779  heibor  37791  rrnequiv  37805  lsatlss  38960  cdleme50rnlem  40509  sticksstones2  42106  aks6d1c6lem5  42136  cmpfiiin  42667  isnacs3  42680  eldioph2lem2  42731  fnwe2lem2  43022  lmhmfgima  43055  cantnfub2  43293  onnog  43400  gneispacern  44109  imo72b2lem2  44138  imo72b2lem1  44140  imo72b2  44143  refsumcn  45002  cncmpmax  45004  elpmrn  45192  climinf  45583  climinf2lem  45683  limsupvaluz2  45715  supcnvlimsup  45717  limsupgtlem  45754  icccncfext  45864  dvsinax  45890  itgsubsticclem  45952  fourierdlem70  46153  fourierdlem82  46165  fge0npnf  46344  sge0resrnlem  46380  sge0isum  46404  sge0seq  46423  meadjiunlem  46442  omeiunle  46494  hoicvr  46525  vonvolmbllem  46637  preimaioomnf  46696  smfco  46779  ackvalsucsucval  48616  aacllem  49613