Theorem frnd 6300

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

Syntax hints:   → wi 4   ⊆ wss 3792  ran crn 5358  ⟶wf 6133

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 199  df-an 387  df-f 6141

This theorem is referenced by:  fliftrel  6832  fun11iun  7407  f1dmex  7417  fo2ndf  7567  onoviun  7725  onnseq  7726  smores2  7736  domdifsn  8333  omxpenlem  8351  fodomr  8401  domss2  8409  sucdom2  8446  f1finf1o  8477  f1fi  8543  unirnffid  8548  intrnfi  8612  dffi3  8627  ordtypelem8  8721  ordtypelem9  8722  ordtypelem10  8723  hartogslem1  8738  brwdom2  8769  unxpwdom2  8784  ixpiunwdom  8787  infdifsn  8853  cantnf  8889  ac10ct  9192  numacn  9207  infpwfien  9220  fictb  9404  isf34lem5  9537  isf34lem7  9538  isf34lem6  9539  enfin1ai  9543  canthp1lem2  9812  gch3  9835  wuncval2  9906  peano5nni  11381  hashimarn  13545  hashf1lem1  13557  hashf1lem2  13558  ccatrn  13683  swrdrn  13750  pfxrn  13798  cshwrn  13957  limsupgle  14620  limsupgre  14624  isercolllem2  14808  isercoll  14810  isercoll2  14811  climsup  14812  ruclem11  15377  4sqlem11  16067  vdwapf  16084  vdwlem11  16103  0ram  16132  funcres2b  16946  funcres2c  16950  setcepi  17127  yoniso  17315  isacs4lem  17558  mhmima  17753  gsumwspan  17774  frmdss2  17791  cycsubgcl  18008  cycsubgss  18009  ghmrn  18061  conjnmz  18082  cntzmhm  18158  f1omvdconj  18253  odf1o2  18376  pgpssslw  18417  sylow2blem1  18423  lsmssv  18446  lsmidm  18465  pj1ghm2  18505  efgsp1  18538  efgrelexlemb  18553  cntzcmnf  18638  cyggenod  18676  gsumval3eu  18695  gsumval3lem2  18697  gsumval3  18698  gsumzsubmcl  18708  gsumzaddlem  18711  gsumzadd  18712  gsumzsplit  18717  gsumconst  18724  gsumzoppg  18734  gsumpt  18751  dmdprdd  18789  dprdfcntz  18805  dprdfeq0  18812  dprdlub  18816  dprdres  18818  dprdss  18819  dprdz  18820  subgdprd  18825  dprd2dlem1  18831  dprd2da  18832  dmdprdsplit2lem  18835  dpjghm2  18854  ablfac1b  18860  lmhmlsp  19448  pj1lmhm2  19500  aspval2  19748  mplcoe5lem  19868  mplbas2  19871  mplind  19902  evlslem1  19915  evlseu  19916  gsumply1subr  20004  pjfo  20462  frlmsplit2  20520  frlmsslsp  20543  frlmlbs  20544  frlmup3  20547  frlmup4  20548  lindff1  20567  lindfrn  20568  f1lindf  20569  indlcim  20587  m2cpmf1  20959  m2cpmghm  20960  iinopn  21118  pptbas  21224  tgrest  21375  resttopon  21377  rest0  21385  restfpw  21395  ordtbaslem  21404  ordtuni  21406  ordtbas2  21407  ordtrest  21418  ordtrest2  21420  cnclsi  21488  cnrest2r  21503  cnprest2  21506  lmss  21514  cncmp  21608  rncmp  21612  discmp  21614  connima  21641  conncn  21642  2ndcdisj  21672  2ndcomap  21674  dis2ndc  21676  lly1stc  21712  comppfsc  21748  kgencmp  21761  1stckgenlem  21769  kgencn3  21774  ptbasfi  21797  txbasval  21822  upxp  21839  uptx  21841  txtube  21856  txcmplem1  21857  txcmplem2  21858  tx1stc  21866  xkoptsub  21870  xkoco2cn  21874  xkococnlem  21875  hmeores  21987  fbasrn  22100  trfilss  22105  trfg  22107  uzrest  22113  rnelfmlem  22168  fclscmpi  22245  alexsublem  22260  ptcmplem1  22268  ptcmplem3  22270  cnextcn  22283  tmdgsum2  22312  subgtgp  22321  subgntr  22322  opnsubg  22323  clsnsg  22325  tgpconncomp  22328  tsmsfbas  22343  prdsdsf  22584  prdsxmetlem  22585  prdsmet  22587  imasdsf1olem  22590  unirnblps  22636  unirnbl  22637  prdsbl  22708  met1stc  22738  met2ndci  22739  prdsxmslem2  22746  xrge0gsumle  23048  xrge0tsms  23049  metdcn2  23054  metdsf  23063  metdsge  23064  cnmptre  23138  bndth  23169  evth  23170  evth2  23171  lebnumlem2  23173  lebnumlem3  23174  reparphti  23208  bcthlem5  23538  minveclem1  23634  minveclem3b  23638  evthicc2  23668  ovolmge0  23685  ovollb  23687  ovolgelb  23688  ovollb2lem  23696  ovollb2  23697  ovolunlem1a  23704  ovolunlem1  23705  ovoliunlem1  23710  ovoliun  23713  ovoliun2  23714  ovolscalem1  23721  ovolicc1  23724  ovolicc2lem4  23728  ovolicc2  23730  voliunlem2  23759  voliunlem3  23760  ioombl1lem2  23767  ioombl1lem4  23769  uniioovol  23787  uniiccvol  23788  uniioombllem1  23789  uniioombllem2  23791  uniioombllem3  23793  uniioombllem6  23796  uniioombl  23797  volsup2  23813  vitalilem2  23817  vitalilem4  23819  vitalilem5  23820  mbfsup  23872  mbfinf  23873  mbflimsup  23874  i1fima  23886  i1fima2  23887  itg1cl  23893  itg1ge0  23894  i1fmullem  23902  i1fadd  23903  i1fmul  23904  itg1addlem4  23907  itg1addlem5  23908  i1fmulc  23911  itg1mulc  23912  i1fres  23913  itg10a  23918  itg1ge0a  23919  itg1climres  23922  mbfi1fseqlem4  23926  itg2seq  23950  itg2monolem1  23958  itg2monolem2  23959  itg2monolem3  23960  itg2mono  23961  itg2i1fseq2  23964  itg2gt0  23968  itg2cnlem1  23969  itg2cn  23971  dvne0  24215  lhop2  24219  mdegleb  24265  mdegldg  24267  aalioulem3  24530  logccv  24850  efrlim  25152  basellem3  25265  fsumvma  25394  lgseisenlem4  25559  uhgredgn0  26480  upgredgss  26484  umgredgss  26485  edgupgr  26486  upgredg  26490  usgruspgrb  26534  upgrres1  26664  ubthlem1  28302  minvecolem1  28306  htthlem  28350  ofrn  30010  ofrn2  30011  xppreima2  30019  fsumiunle  30143  xrge0tsmsd  30351  cmpcref  30519  ordtrestNEW  30569  ordtrest2NEW  30571  xrge0mulc1cn  30589  rge0scvg  30597  esumcst  30727  esumpfinvallem  30738  esumpcvgval  30742  esumiun  30758  omssubadd  30964  carsggect  30982  sibfinima  31003  sitgclg  31006  sitgaddlemb  31012  eulerpartgbij  31036  rrvrnss  31112  orvcval4  31125  erdsze2lem2  31789  cvxpconn  31827  cvxsconn  31828  cvmsss2  31859  cvmliftlem8  31877  cvmlift3lem6  31909  mrsubrn  32013  msubrn  32029  mvtss  32053  mclsssvlem  32062  mclsax  32069  mclsind  32070  neibastop2lem  32947  tailfb  32964  knoppcnlem10  33079  lindsdom  34034  poimirlem2  34042  poimirlem11  34051  poimirlem19  34059  poimirlem27  34067  poimirlem30  34070  mblfinlem2  34078  itg2addnclem2  34092  itg2gt0cn  34095  ftc1anclem3  34117  ftc1anclem6  34120  ftc1anclem7  34121  ftc1anc  34123  cnresima  34192  istotbnd3  34199  sstotbnd2  34202  totbndbnd  34217  prdsbnd  34221  cntotbnd  34224  ismtyima  34231  heibor1lem  34237  heibor  34249  rrnequiv  34263  lsatlss  35155  cdleme50rnlem  36703  cmpfiiin  38230  isnacs3  38243  eldioph2lem2  38294  fnwe2lem2  38590  lmhmfgima  38623  imo72b2lem0  39431  imo72b2lem2  39433  imo72b2lem1  39437  imo72b2  39441  refsumcn  40132  cncmpmax  40134  elpmrn  40345  climinf  40756  climinf2lem  40856  limsupvaluz2  40888  supcnvlimsup  40890  limsupgtlem  40927  icccncfext  41038  dvsinax  41065  itgsubsticclem  41128  fourierdlem70  41330  fourierdlem82  41342  fge0npnf  41518  sge0resrnlem  41554  sge0isum  41578  sge0seq  41597  meadjiunlem  41616  omeiunle  41668  hoicvr  41699  vonvolmbllem  41811  preimaioomnf  41866  smfco  41946  mgmhmima  42827  aacllem  43663