Theorem frnd 6723

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

Syntax hints:   → wi 4   ⊆ wss 3948  ran crn 5677  ⟶wf 6537

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 398  df-f 6545

This theorem is referenced by:  f1un  6851  fliftrel  7302  f1iun  7927  f1dmex  7940  fo2ndf  8104  onoviun  8340  onnseq  8341  smores2  8351  domdifsn  9051  omxpenlem  9070  sucdom2OLD  9079  fodomr  9125  domss2  9133  f1domfi  9181  sucdom2  9203  f1finf1o  9268  f1finf1oOLD  9269  infn0  9304  f1fi  9336  unirnffid  9341  intrnfi  9408  dffi3  9423  ordtypelem8  9517  ordtypelem9  9518  ordtypelem10  9519  hartogslem1  9534  brwdom2  9565  unxpwdom2  9580  ixpiunwdom  9582  infdifsn  9649  cantnf  9685  ac10ct  10026  numacn  10041  infpwfien  10054  fictb  10237  isf34lem5  10370  isf34lem7  10371  isf34lem6  10372  enfin1ai  10376  canthp1lem2  10645  gch3  10668  wuncval2  10739  peano5nni  12212  hashimarn  14397  hashf1lem1  14412  hashf1lem1OLD  14413  hashf1lem2  14414  ccatrn  14536  swrdrn  14599  pfxrn  14632  cshwrn  14749  limsupgle  15418  limsupgre  15422  isercolllem2  15609  isercoll  15611  isercoll2  15612  climsup  15613  ruclem11  16180  4sqlem11  16885  vdwapf  16902  vdwlem11  16921  0ram  16950  funcres2b  17844  funcres2c  17849  setcepi  18035  yoniso  18235  isacs4lem  18494  mhmima  18703  gsumwspan  18724  frmdss2  18741  cycsubm  19074  cycsubgcl  19078  cycsubgss  19079  ghmrn  19100  conjnmz  19121  cntzmhm  19200  f1omvdconj  19309  odf1o2  19436  pgpssslw  19477  sylow2blem1  19483  lsmssv  19506  smndlsmidm  19519  pj1ghm2  19567  efgsp1  19600  efgrelexlemb  19613  cntzcmnf  19708  cyggenod  19747  gsumval3eu  19767  gsumval3lem2  19769  gsumval3  19770  gsumzsubmcl  19781  gsumzaddlem  19784  gsumzadd  19785  gsumzsplit  19790  gsumconst  19797  gsumzoppg  19807  gsumpt  19825  dmdprdd  19864  dprdfcntz  19880  dprdfeq0  19887  dprdlub  19891  dprdres  19893  dprdss  19894  dprdz  19895  subgdprd  19900  dprd2dlem1  19906  dprd2da  19907  dmdprdsplit2lem  19910  dpjghm2  19929  ablfac1b  19935  lmhmlsp  20653  pj1lmhm2  20705  pjfo  21262  frlmsplit2  21320  frlmsslsp  21343  frlmlbs  21344  frlmup3  21347  frlmup4  21348  lindff1  21367  lindfrn  21368  f1lindf  21369  indlcim  21387  aspval2  21444  mplcoe5lem  21586  mplbas2  21589  mplind  21623  evlslem1  21637  evlseu  21638  gsumply1subr  21748  m2cpmf1  22237  m2cpmghm  22238  iinopn  22396  pptbas  22503  tgrest  22655  resttopon  22657  rest0  22665  restfpw  22675  ordtbaslem  22684  ordtuni  22686  ordtbas2  22687  ordtrest  22698  ordtrest2  22700  cnclsi  22768  cnrest2r  22783  cnprest2  22786  lmss  22794  cncmp  22888  rncmp  22892  discmp  22894  connima  22921  conncn  22922  2ndcdisj  22952  2ndcomap  22954  dis2ndc  22956  lly1stc  22992  comppfsc  23028  kgencmp  23041  1stckgenlem  23049  kgencn3  23054  ptbasfi  23077  txbasval  23102  upxp  23119  uptx  23121  txtube  23136  txcmplem1  23137  txcmplem2  23138  tx1stc  23146  xkoptsub  23150  xkoco2cn  23154  xkococnlem  23155  hmeores  23267  fbasrn  23380  trfilss  23385  trfg  23387  uzrest  23393  rnelfmlem  23448  fclscmpi  23525  alexsublem  23540  ptcmplem1  23548  ptcmplem3  23550  cnextcn  23563  tmdgsum2  23592  subgtgp  23601  subgntr  23603  opnsubg  23604  clsnsg  23606  tgpconncomp  23609  tsmsfbas  23624  prdsdsf  23865  prdsxmetlem  23866  prdsmet  23868  imasdsf1olem  23871  unirnblps  23917  unirnbl  23918  prdsbl  23992  met1stc  24022  met2ndci  24023  prdsxmslem2  24030  xrge0gsumle  24341  xrge0tsms  24342  metdcn2  24347  metdsf  24356  metdsge  24357  cnmptre  24435  bndth  24466  evth  24467  evth2  24468  lebnumlem2  24470  lebnumlem3  24471  reparphti  24505  bcthlem5  24837  minveclem1  24933  minveclem3b  24937  evthicc2  24969  ovolmge0  24986  ovollb  24988  ovolgelb  24989  ovollb2lem  24997  ovollb2  24998  ovolunlem1a  25005  ovolunlem1  25006  ovoliunlem1  25011  ovoliun  25014  ovoliun2  25015  ovolscalem1  25022  ovolicc1  25025  ovolicc2lem4  25029  ovolicc2  25031  voliunlem2  25060  voliunlem3  25061  ioombl1lem2  25068  ioombl1lem4  25070  uniioovol  25088  uniiccvol  25089  uniioombllem1  25090  uniioombllem2  25092  uniioombllem3  25094  uniioombllem6  25097  uniioombl  25098  volsup2  25114  vitalilem2  25118  vitalilem4  25120  vitalilem5  25121  mbfsup  25173  mbfinf  25174  mbflimsup  25175  i1fima  25187  i1fima2  25188  itg1cl  25194  itg1ge0  25195  i1fmullem  25203  i1fadd  25204  i1fmul  25205  itg1addlem4  25208  itg1addlem4OLD  25209  itg1addlem5  25210  i1fmulc  25213  itg1mulc  25214  i1fres  25215  itg10a  25220  itg1ge0a  25221  itg1climres  25224  mbfi1fseqlem4  25228  itg2seq  25252  itg2monolem1  25260  itg2monolem2  25261  itg2monolem3  25262  itg2mono  25263  itg2i1fseq2  25266  itg2gt0  25270  itg2cnlem1  25271  itg2cn  25273  dvne0  25520  lhop2  25524  mdegleb  25574  mdegldg  25576  aalioulem3  25839  logccv  26163  efrlim  26464  basellem3  26577  fsumvma  26706  lgseisenlem4  26871  uhgredgn0  28378  upgredgss  28382  umgredgss  28383  edgupgr  28384  upgredg  28387  usgruspgrb  28431  upgrres1  28560  ubthlem1  30111  minvecolem1  30115  htthlem  30158  ofrn  31852  ofrn2  31853  xppreima2  31864  fsumiunle  32023  mgcf1o  32161  gsumhashmul  32196  xrge0tsmsd  32197  symgcom  32232  cycpmcl  32263  cycpmco2lem1  32273  cycpmco2lem5  32277  cycpmco2  32280  cycpmconjv  32289  cycpmconjslem2  32302  ghmquskerlem3  32520  ply1degltdimlem  32696  cmpcref  32819  ordtrestNEW  32890  ordtrest2NEW  32892  xrge0mulc1cn  32910  rge0scvg  32918  esumcst  33050  esumpfinvallem  33061  esumpcvgval  33065  esumiun  33081  omssubadd  33288  carsggect  33306  sibfinima  33327  sitgclg  33330  sitgaddlemb  33336  eulerpartgbij  33360  rrvrnss  33435  orvcval4  33448  erdsze2lem2  34184  cvxpconn  34222  cvxsconn  34223  cvmsss2  34254  cvmliftlem8  34272  cvmlift3lem6  34304  mrsubrn  34493  msubrn  34509  mvtss  34533  mclsssvlem  34542  mclsax  34549  mclsind  34550  gg-reparphti  35161  neibastop2lem  35234  tailfb  35251  knoppcnlem10  35367  lindsdom  36471  poimirlem2  36479  poimirlem11  36488  poimirlem19  36496  poimirlem27  36504  poimirlem30  36507  mblfinlem2  36515  itg2addnclem2  36529  itg2gt0cn  36532  ftc1anclem3  36552  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anc  36558  cnresima  36621  istotbnd3  36628  sstotbnd2  36631  totbndbnd  36646  prdsbnd  36650  cntotbnd  36653  ismtyima  36660  heibor1lem  36666  heibor  36678  rrnequiv  36692  lsatlss  37855  cdleme50rnlem  39404  sticksstones2  40952  cmpfiiin  41421  isnacs3  41434  eldioph2lem2  41485  fnwe2lem2  41779  lmhmfgima  41812  cantnfub2  42058  onnog  42166  gneispacern  42875  imo72b2lem0  42903  imo72b2lem2  42905  imo72b2lem1  42907  imo72b2  42910  refsumcn  43700  cncmpmax  43702  elpmrn  43905  climinf  44309  climinf2lem  44409  limsupvaluz2  44441  supcnvlimsup  44443  limsupgtlem  44480  icccncfext  44590  dvsinax  44616  itgsubsticclem  44678  fourierdlem70  44879  fourierdlem82  44891  fge0npnf  45070  sge0resrnlem  45106  sge0isum  45130  sge0seq  45149  meadjiunlem  45168  omeiunle  45220  hoicvr  45251  vonvolmbllem  45363  preimaioomnf  45422  smfco  45505  mgmhmima  46559  ackvalsucsucval  47328  aacllem  47802