Theorem frnd 6523

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

Syntax hints:   → wi 4   ⊆ wss 3938  ran crn 5558  ⟶wf 6353

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 209  df-an 399  df-f 6361

This theorem is referenced by:  fliftrel  7063  f1iun  7647  f1dmex  7660  fo2ndf  7819  onoviun  7982  onnseq  7983  smores2  7993  domdifsn  8602  omxpenlem  8620  fodomr  8670  domss2  8678  sucdom2  8716  f1finf1o  8747  f1fi  8813  unirnffid  8818  intrnfi  8882  dffi3  8897  ordtypelem8  8991  ordtypelem9  8992  ordtypelem10  8993  hartogslem1  9008  brwdom2  9039  unxpwdom2  9054  ixpiunwdom  9057  infdifsn  9122  cantnf  9158  ac10ct  9462  numacn  9477  infpwfien  9490  fictb  9669  isf34lem5  9802  isf34lem7  9803  isf34lem6  9804  enfin1ai  9808  canthp1lem2  10077  gch3  10100  wuncval2  10171  peano5nni  11643  hashimarn  13804  hashf1lem1  13816  hashf1lem2  13817  ccatrn  13945  swrdrn  14016  pfxrn  14049  cshwrn  14166  limsupgle  14836  limsupgre  14840  isercolllem2  15024  isercoll  15026  isercoll2  15027  climsup  15028  ruclem11  15595  4sqlem11  16293  vdwapf  16310  vdwlem11  16329  0ram  16358  funcres2b  17169  funcres2c  17173  setcepi  17350  yoniso  17537  isacs4lem  17780  mhmima  17991  gsumwspan  18013  frmdss2  18030  cycsubm  18347  cycsubgcl  18351  cycsubgss  18352  ghmrn  18373  conjnmz  18394  cntzmhm  18471  f1omvdconj  18576  odf1o2  18700  pgpssslw  18741  sylow2blem1  18747  lsmssv  18770  smndlsmidm  18783  lsmidmOLD  18791  pj1ghm2  18832  efgsp1  18865  efgrelexlemb  18878  cntzcmnf  18967  cyggenod  19005  gsumval3eu  19026  gsumval3lem2  19028  gsumval3  19029  gsumzsubmcl  19040  gsumzaddlem  19043  gsumzadd  19044  gsumzsplit  19049  gsumconst  19056  gsumzoppg  19066  gsumpt  19084  dmdprdd  19123  dprdfcntz  19139  dprdfeq0  19146  dprdlub  19150  dprdres  19152  dprdss  19153  dprdz  19154  subgdprd  19159  dprd2dlem1  19165  dprd2da  19166  dmdprdsplit2lem  19169  dpjghm2  19188  ablfac1b  19194  lmhmlsp  19823  pj1lmhm2  19875  aspval2  20129  mplcoe5lem  20250  mplbas2  20253  mplind  20284  evlslem1  20297  evlseu  20298  gsumply1subr  20404  pjfo  20861  frlmsplit2  20919  frlmsslsp  20942  frlmlbs  20943  frlmup3  20946  frlmup4  20947  lindff1  20966  lindfrn  20967  f1lindf  20968  indlcim  20986  m2cpmf1  21353  m2cpmghm  21354  iinopn  21512  pptbas  21618  tgrest  21769  resttopon  21771  rest0  21779  restfpw  21789  ordtbaslem  21798  ordtuni  21800  ordtbas2  21801  ordtrest  21812  ordtrest2  21814  cnclsi  21882  cnrest2r  21897  cnprest2  21900  lmss  21908  cncmp  22002  rncmp  22006  discmp  22008  connima  22035  conncn  22036  2ndcdisj  22066  2ndcomap  22068  dis2ndc  22070  lly1stc  22106  comppfsc  22142  kgencmp  22155  1stckgenlem  22163  kgencn3  22168  ptbasfi  22191  txbasval  22216  upxp  22233  uptx  22235  txtube  22250  txcmplem1  22251  txcmplem2  22252  tx1stc  22260  xkoptsub  22264  xkoco2cn  22268  xkococnlem  22269  hmeores  22381  fbasrn  22494  trfilss  22499  trfg  22501  uzrest  22507  rnelfmlem  22562  fclscmpi  22639  alexsublem  22654  ptcmplem1  22662  ptcmplem3  22664  cnextcn  22677  tmdgsum2  22706  subgtgp  22715  subgntr  22717  opnsubg  22718  clsnsg  22720  tgpconncomp  22723  tsmsfbas  22738  prdsdsf  22979  prdsxmetlem  22980  prdsmet  22982  imasdsf1olem  22985  unirnblps  23031  unirnbl  23032  prdsbl  23103  met1stc  23133  met2ndci  23134  prdsxmslem2  23141  xrge0gsumle  23443  xrge0tsms  23444  metdcn2  23449  metdsf  23458  metdsge  23459  cnmptre  23533  bndth  23564  evth  23565  evth2  23566  lebnumlem2  23568  lebnumlem3  23569  reparphti  23603  bcthlem5  23933  minveclem1  24029  minveclem3b  24033  evthicc2  24063  ovolmge0  24080  ovollb  24082  ovolgelb  24083  ovollb2lem  24091  ovollb2  24092  ovolunlem1a  24099  ovolunlem1  24100  ovoliunlem1  24105  ovoliun  24108  ovoliun2  24109  ovolscalem1  24116  ovolicc1  24119  ovolicc2lem4  24123  ovolicc2  24125  voliunlem2  24154  voliunlem3  24155  ioombl1lem2  24162  ioombl1lem4  24164  uniioovol  24182  uniiccvol  24183  uniioombllem1  24184  uniioombllem2  24186  uniioombllem3  24188  uniioombllem6  24191  uniioombl  24192  volsup2  24208  vitalilem2  24212  vitalilem4  24214  vitalilem5  24215  mbfsup  24267  mbfinf  24268  mbflimsup  24269  i1fima  24281  i1fima2  24282  itg1cl  24288  itg1ge0  24289  i1fmullem  24297  i1fadd  24298  i1fmul  24299  itg1addlem4  24302  itg1addlem5  24303  i1fmulc  24306  itg1mulc  24307  i1fres  24308  itg10a  24313  itg1ge0a  24314  itg1climres  24317  mbfi1fseqlem4  24321  itg2seq  24345  itg2monolem1  24353  itg2monolem2  24354  itg2monolem3  24355  itg2mono  24356  itg2i1fseq2  24359  itg2gt0  24363  itg2cnlem1  24364  itg2cn  24366  dvne0  24610  lhop2  24614  mdegleb  24660  mdegldg  24662  aalioulem3  24925  logccv  25248  efrlim  25549  basellem3  25662  fsumvma  25791  lgseisenlem4  25956  uhgredgn0  26915  upgredgss  26919  umgredgss  26920  edgupgr  26921  upgredg  26924  usgruspgrb  26968  upgrres1  27097  ubthlem1  28649  minvecolem1  28653  htthlem  28696  ofrn  30388  ofrn2  30389  xppreima2  30397  fsumiunle  30547  xrge0tsmsd  30694  symgcom  30729  cycpmcl  30760  cycpmco2lem1  30770  cycpmco2lem5  30774  cycpmco2  30777  cycpmconjv  30786  cycpmconjslem2  30799  cmpcref  31116  ordtrestNEW  31166  ordtrest2NEW  31168  xrge0mulc1cn  31186  rge0scvg  31194  esumcst  31324  esumpfinvallem  31335  esumpcvgval  31339  esumiun  31355  omssubadd  31560  carsggect  31578  sibfinima  31599  sitgclg  31602  sitgaddlemb  31608  eulerpartgbij  31632  rrvrnss  31707  orvcval4  31720  erdsze2lem2  32453  cvxpconn  32491  cvxsconn  32492  cvmsss2  32523  cvmliftlem8  32541  cvmlift3lem6  32573  mrsubrn  32762  msubrn  32778  mvtss  32802  mclsssvlem  32811  mclsax  32818  mclsind  32819  neibastop2lem  33710  tailfb  33727  knoppcnlem10  33843  lindsdom  34888  poimirlem2  34896  poimirlem11  34905  poimirlem19  34913  poimirlem27  34921  poimirlem30  34924  mblfinlem2  34932  itg2addnclem2  34946  itg2gt0cn  34949  ftc1anclem3  34971  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anc  34977  cnresima  35044  istotbnd3  35051  sstotbnd2  35054  totbndbnd  35069  prdsbnd  35073  cntotbnd  35076  ismtyima  35083  heibor1lem  35089  heibor  35101  rrnequiv  35115  lsatlss  36134  cdleme50rnlem  37682  cmpfiiin  39301  isnacs3  39314  eldioph2lem2  39365  fnwe2lem2  39658  lmhmfgima  39691  gneispacern  40495  imo72b2lem0  40523  imo72b2lem2  40525  imo72b2lem1  40528  imo72b2  40532  refsumcn  41294  cncmpmax  41296  elpmrn  41492  climinf  41894  climinf2lem  41994  limsupvaluz2  42026  supcnvlimsup  42028  limsupgtlem  42065  icccncfext  42177  dvsinax  42204  itgsubsticclem  42267  fourierdlem70  42468  fourierdlem82  42480  fge0npnf  42656  sge0resrnlem  42692  sge0isum  42716  sge0seq  42735  meadjiunlem  42754  omeiunle  42806  hoicvr  42837  vonvolmbllem  42949  preimaioomnf  43004  smfco  43084  mgmhmima  44076  aacllem  44909