Theorem frnd 6735

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

Syntax hints:   → wi 4   ⊆ wss 3949  ran crn 5683  ⟶wf 6549

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 206  df-an 395  df-f 6557

This theorem is referenced by:  f1un  6864  fliftrel  7322  f1iun  7953  f1dmex  7966  fo2ndf  8132  onoviun  8370  onnseq  8371  smores2  8381  domdifsn  9085  omxpenlem  9104  sucdom2OLD  9113  fodomr  9159  domss2  9167  f1domfi  9215  sucdom2  9237  f1finf1o  9302  f1finf1oOLD  9303  infn0  9338  f1fi  9371  unirnffid  9376  intrnfi  9447  dffi3  9462  ordtypelem8  9556  ordtypelem9  9557  ordtypelem10  9558  hartogslem1  9573  brwdom2  9604  unxpwdom2  9619  ixpiunwdom  9621  infdifsn  9688  cantnf  9724  ac10ct  10065  numacn  10080  infpwfien  10093  fictb  10276  isf34lem5  10409  isf34lem7  10410  isf34lem6  10411  enfin1ai  10415  canthp1lem2  10684  gch3  10707  wuncval2  10778  peano5nni  12253  hashimarn  14439  hashf1lem1  14455  hashf1lem1OLD  14456  hashf1lem2  14457  ccatrn  14579  swrdrn  14642  pfxrn  14675  cshwrn  14792  limsupgle  15461  limsupgre  15465  isercolllem2  15652  isercoll  15654  isercoll2  15655  climsup  15656  ruclem11  16224  4sqlem11  16931  vdwapf  16948  vdwlem11  16967  0ram  16996  funcres2b  17890  funcres2c  17897  setcepi  18084  yoniso  18284  isacs4lem  18543  mgmhmima  18682  mhmima  18784  gsumwspan  18805  frmdss2  18822  cycsubm  19164  cycsubgcl  19168  cycsubgss  19169  ghmrn  19190  conjnmz  19213  ghmquskerlem3  19244  cntzmhm  19299  f1omvdconj  19408  odf1o2  19535  pgpssslw  19576  sylow2blem1  19582  lsmssv  19605  smndlsmidm  19618  pj1ghm2  19666  efgsp1  19699  efgrelexlemb  19712  cntzcmnf  19807  cyggenod  19846  gsumval3eu  19866  gsumval3lem2  19868  gsumval3  19869  gsumzsubmcl  19880  gsumzaddlem  19883  gsumzadd  19884  gsumzsplit  19889  gsumconst  19896  gsumzoppg  19906  gsumpt  19924  dmdprdd  19963  dprdfcntz  19979  dprdfeq0  19986  dprdlub  19990  dprdres  19992  dprdss  19993  dprdz  19994  subgdprd  19999  dprd2dlem1  20005  dprd2da  20006  dmdprdsplit2lem  20009  dpjghm2  20028  ablfac1b  20034  lmhmlsp  20941  pj1lmhm2  20993  pjfo  21656  frlmsplit2  21714  frlmsslsp  21737  frlmlbs  21738  frlmup3  21741  frlmup4  21742  lindff1  21761  lindfrn  21762  f1lindf  21763  indlcim  21781  aspval2  21838  mplcoe5lem  21984  mplbas2  21987  mplind  22021  evlslem1  22035  evlseu  22036  gsumply1subr  22159  m2cpmf1  22665  m2cpmghm  22666  iinopn  22824  pptbas  22931  tgrest  23083  resttopon  23085  rest0  23093  restfpw  23103  ordtbaslem  23112  ordtuni  23114  ordtbas2  23115  ordtrest  23126  ordtrest2  23128  cnclsi  23196  cnrest2r  23211  cnprest2  23214  lmss  23222  cncmp  23316  rncmp  23320  discmp  23322  connima  23349  conncn  23350  2ndcdisj  23380  2ndcomap  23382  dis2ndc  23384  lly1stc  23420  comppfsc  23456  kgencmp  23469  1stckgenlem  23477  kgencn3  23482  ptbasfi  23505  txbasval  23530  upxp  23547  uptx  23549  txtube  23564  txcmplem1  23565  txcmplem2  23566  tx1stc  23574  xkoptsub  23578  xkoco2cn  23582  xkococnlem  23583  hmeores  23695  fbasrn  23808  trfilss  23813  trfg  23815  uzrest  23821  rnelfmlem  23876  fclscmpi  23953  alexsublem  23968  ptcmplem1  23976  ptcmplem3  23978  cnextcn  23991  tmdgsum2  24020  subgtgp  24029  subgntr  24031  opnsubg  24032  clsnsg  24034  tgpconncomp  24037  tsmsfbas  24052  prdsdsf  24293  prdsxmetlem  24294  prdsmet  24296  imasdsf1olem  24299  unirnblps  24345  unirnbl  24346  prdsbl  24420  met1stc  24450  met2ndci  24451  prdsxmslem2  24458  xrge0gsumle  24769  xrge0tsms  24770  metdcn2  24775  metdsf  24784  metdsge  24785  cnmptre  24868  bndth  24904  evth  24905  evth2  24906  lebnumlem2  24908  lebnumlem3  24909  reparphti  24943  reparphtiOLD  24944  bcthlem5  25276  minveclem1  25372  minveclem3b  25376  evthicc2  25409  ovolmge0  25426  ovollb  25428  ovolgelb  25429  ovollb2lem  25437  ovollb2  25438  ovolunlem1a  25445  ovolunlem1  25446  ovoliunlem1  25451  ovoliun  25454  ovoliun2  25455  ovolscalem1  25462  ovolicc1  25465  ovolicc2lem4  25469  ovolicc2  25471  voliunlem2  25500  voliunlem3  25501  ioombl1lem2  25508  ioombl1lem4  25510  uniioovol  25528  uniiccvol  25529  uniioombllem1  25530  uniioombllem2  25532  uniioombllem3  25534  uniioombllem6  25537  uniioombl  25538  volsup2  25554  vitalilem2  25558  vitalilem4  25560  vitalilem5  25561  mbfsup  25613  mbfinf  25614  mbflimsup  25615  i1fima  25627  i1fima2  25628  itg1cl  25634  itg1ge0  25635  i1fmullem  25643  i1fadd  25644  i1fmul  25645  itg1addlem4  25648  itg1addlem4OLD  25649  itg1addlem5  25650  i1fmulc  25653  itg1mulc  25654  i1fres  25655  itg10a  25660  itg1ge0a  25661  itg1climres  25664  mbfi1fseqlem4  25668  itg2seq  25692  itg2monolem1  25700  itg2monolem2  25701  itg2monolem3  25702  itg2mono  25703  itg2i1fseq2  25706  itg2gt0  25710  itg2cnlem1  25711  itg2cn  25713  dvne0  25964  lhop2  25968  mdegleb  26020  mdegldg  26022  aalioulem3  26289  logccv  26617  efrlim  26921  efrlimOLD  26922  basellem3  27035  fsumvma  27166  lgseisenlem4  27331  noseqind  28185  uhgredgn0  28961  upgredgss  28965  umgredgss  28966  edgupgr  28967  upgredg  28970  usgruspgrb  29016  upgrres1  29146  ubthlem1  30700  minvecolem1  30704  htthlem  30747  ofrn  32446  ofrn2  32447  xppreima2  32458  fsumiunle  32613  mgcf1o  32751  gsumhashmul  32791  xrge0tsmsd  32792  symgcom  32827  cycpmcl  32858  cycpmco2lem1  32868  cycpmco2lem5  32872  cycpmco2  32875  cycpmconjv  32884  cycpmconjslem2  32897  idomsubr  33020  ghmqusnsg  33156  ply1degltdimlem  33353  cmpcref  33484  ordtrestNEW  33555  ordtrest2NEW  33557  xrge0mulc1cn  33575  rge0scvg  33583  esumcst  33715  esumpfinvallem  33726  esumpcvgval  33730  esumiun  33746  omssubadd  33953  carsggect  33971  sibfinima  33992  sitgclg  33995  sitgaddlemb  34001  eulerpartgbij  34025  rrvrnss  34100  orvcval4  34113  erdsze2lem2  34847  cvxpconn  34885  cvxsconn  34886  cvmsss2  34917  cvmliftlem8  34935  cvmlift3lem6  34967  mrsubrn  35156  msubrn  35172  mvtss  35196  mclsssvlem  35205  mclsax  35212  mclsind  35213  neibastop2lem  35877  tailfb  35894  knoppcnlem10  36010  lindsdom  37120  poimirlem2  37128  poimirlem11  37137  poimirlem19  37145  poimirlem27  37153  poimirlem30  37156  mblfinlem2  37164  itg2addnclem2  37178  itg2gt0cn  37181  ftc1anclem3  37201  ftc1anclem6  37204  ftc1anclem7  37205  ftc1anc  37207  cnresima  37270  istotbnd3  37277  sstotbnd2  37280  totbndbnd  37295  prdsbnd  37299  cntotbnd  37302  ismtyima  37309  heibor1lem  37315  heibor  37327  rrnequiv  37341  lsatlss  38500  cdleme50rnlem  40049  sticksstones2  41651  aks6d1c6lem5  41681  cmpfiiin  42148  isnacs3  42161  eldioph2lem2  42212  fnwe2lem2  42506  lmhmfgima  42539  cantnfub2  42782  onnog  42890  gneispacern  43599  imo72b2lem0  43626  imo72b2lem2  43628  imo72b2lem1  43630  imo72b2  43633  refsumcn  44423  cncmpmax  44425  elpmrn  44623  climinf  45023  climinf2lem  45123  limsupvaluz2  45155  supcnvlimsup  45157  limsupgtlem  45194  icccncfext  45304  dvsinax  45330  itgsubsticclem  45392  fourierdlem70  45593  fourierdlem82  45605  fge0npnf  45784  sge0resrnlem  45820  sge0isum  45844  sge0seq  45863  meadjiunlem  45882  omeiunle  45934  hoicvr  45965  vonvolmbllem  46077  preimaioomnf  46136  smfco  46219  ackvalsucsucval  47839  aacllem  48312