Theorem frnd 6521

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

Syntax hints:   → wi 4   ⊆ wss 3936  ran crn 5556  ⟶wf 6351

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 6359

This theorem is referenced by:  fliftrel  7061  f1iun  7645  f1dmex  7658  fo2ndf  7817  onoviun  7980  onnseq  7981  smores2  7991  domdifsn  8600  omxpenlem  8618  fodomr  8668  domss2  8676  sucdom2  8714  f1finf1o  8745  f1fi  8811  unirnffid  8816  intrnfi  8880  dffi3  8895  ordtypelem8  8989  ordtypelem9  8990  ordtypelem10  8991  hartogslem1  9006  brwdom2  9037  unxpwdom2  9052  ixpiunwdom  9055  infdifsn  9120  cantnf  9156  ac10ct  9460  numacn  9475  infpwfien  9488  fictb  9667  isf34lem5  9800  isf34lem7  9801  isf34lem6  9802  enfin1ai  9806  canthp1lem2  10075  gch3  10098  wuncval2  10169  peano5nni  11641  hashimarn  13802  hashf1lem1  13814  hashf1lem2  13815  ccatrn  13943  swrdrn  14014  pfxrn  14047  cshwrn  14164  limsupgle  14834  limsupgre  14838  isercolllem2  15022  isercoll  15024  isercoll2  15025  climsup  15026  ruclem11  15593  4sqlem11  16291  vdwapf  16308  vdwlem11  16327  0ram  16356  funcres2b  17167  funcres2c  17171  setcepi  17348  yoniso  17535  isacs4lem  17778  mhmima  17989  gsumwspan  18011  frmdss2  18028  cycsubm  18345  cycsubgcl  18349  cycsubgss  18350  ghmrn  18371  conjnmz  18392  cntzmhm  18469  f1omvdconj  18574  odf1o2  18698  pgpssslw  18739  sylow2blem1  18745  lsmssv  18768  smndlsmidm  18781  lsmidmOLD  18789  pj1ghm2  18830  efgsp1  18863  efgrelexlemb  18876  cntzcmnf  18965  cyggenod  19003  gsumval3eu  19024  gsumval3lem2  19026  gsumval3  19027  gsumzsubmcl  19038  gsumzaddlem  19041  gsumzadd  19042  gsumzsplit  19047  gsumconst  19054  gsumzoppg  19064  gsumpt  19082  dmdprdd  19121  dprdfcntz  19137  dprdfeq0  19144  dprdlub  19148  dprdres  19150  dprdss  19151  dprdz  19152  subgdprd  19157  dprd2dlem1  19163  dprd2da  19164  dmdprdsplit2lem  19167  dpjghm2  19186  ablfac1b  19192  lmhmlsp  19821  pj1lmhm2  19873  aspval2  20127  mplcoe5lem  20248  mplbas2  20251  mplind  20282  evlslem1  20295  evlseu  20296  gsumply1subr  20402  pjfo  20859  frlmsplit2  20917  frlmsslsp  20940  frlmlbs  20941  frlmup3  20944  frlmup4  20945  lindff1  20964  lindfrn  20965  f1lindf  20966  indlcim  20984  m2cpmf1  21351  m2cpmghm  21352  iinopn  21510  pptbas  21616  tgrest  21767  resttopon  21769  rest0  21777  restfpw  21787  ordtbaslem  21796  ordtuni  21798  ordtbas2  21799  ordtrest  21810  ordtrest2  21812  cnclsi  21880  cnrest2r  21895  cnprest2  21898  lmss  21906  cncmp  22000  rncmp  22004  discmp  22006  connima  22033  conncn  22034  2ndcdisj  22064  2ndcomap  22066  dis2ndc  22068  lly1stc  22104  comppfsc  22140  kgencmp  22153  1stckgenlem  22161  kgencn3  22166  ptbasfi  22189  txbasval  22214  upxp  22231  uptx  22233  txtube  22248  txcmplem1  22249  txcmplem2  22250  tx1stc  22258  xkoptsub  22262  xkoco2cn  22266  xkococnlem  22267  hmeores  22379  fbasrn  22492  trfilss  22497  trfg  22499  uzrest  22505  rnelfmlem  22560  fclscmpi  22637  alexsublem  22652  ptcmplem1  22660  ptcmplem3  22662  cnextcn  22675  tmdgsum2  22704  subgtgp  22713  subgntr  22715  opnsubg  22716  clsnsg  22718  tgpconncomp  22721  tsmsfbas  22736  prdsdsf  22977  prdsxmetlem  22978  prdsmet  22980  imasdsf1olem  22983  unirnblps  23029  unirnbl  23030  prdsbl  23101  met1stc  23131  met2ndci  23132  prdsxmslem2  23139  xrge0gsumle  23441  xrge0tsms  23442  metdcn2  23447  metdsf  23456  metdsge  23457  cnmptre  23531  bndth  23562  evth  23563  evth2  23564  lebnumlem2  23566  lebnumlem3  23567  reparphti  23601  bcthlem5  23931  minveclem1  24027  minveclem3b  24031  evthicc2  24061  ovolmge0  24078  ovollb  24080  ovolgelb  24081  ovollb2lem  24089  ovollb2  24090  ovolunlem1a  24097  ovolunlem1  24098  ovoliunlem1  24103  ovoliun  24106  ovoliun2  24107  ovolscalem1  24114  ovolicc1  24117  ovolicc2lem4  24121  ovolicc2  24123  voliunlem2  24152  voliunlem3  24153  ioombl1lem2  24160  ioombl1lem4  24162  uniioovol  24180  uniiccvol  24181  uniioombllem1  24182  uniioombllem2  24184  uniioombllem3  24186  uniioombllem6  24189  uniioombl  24190  volsup2  24206  vitalilem2  24210  vitalilem4  24212  vitalilem5  24213  mbfsup  24265  mbfinf  24266  mbflimsup  24267  i1fima  24279  i1fima2  24280  itg1cl  24286  itg1ge0  24287  i1fmullem  24295  i1fadd  24296  i1fmul  24297  itg1addlem4  24300  itg1addlem5  24301  i1fmulc  24304  itg1mulc  24305  i1fres  24306  itg10a  24311  itg1ge0a  24312  itg1climres  24315  mbfi1fseqlem4  24319  itg2seq  24343  itg2monolem1  24351  itg2monolem2  24352  itg2monolem3  24353  itg2mono  24354  itg2i1fseq2  24357  itg2gt0  24361  itg2cnlem1  24362  itg2cn  24364  dvne0  24608  lhop2  24612  mdegleb  24658  mdegldg  24660  aalioulem3  24923  logccv  25246  efrlim  25547  basellem3  25660  fsumvma  25789  lgseisenlem4  25954  uhgredgn0  26913  upgredgss  26917  umgredgss  26918  edgupgr  26919  upgredg  26922  usgruspgrb  26966  upgrres1  27095  ubthlem1  28647  minvecolem1  28651  htthlem  28694  ofrn  30386  ofrn2  30387  xppreima2  30395  fsumiunle  30545  xrge0tsmsd  30692  symgcom  30727  cycpmcl  30758  cycpmco2lem1  30768  cycpmco2lem5  30772  cycpmco2  30775  cycpmconjv  30784  cycpmconjslem2  30797  cmpcref  31114  ordtrestNEW  31164  ordtrest2NEW  31166  xrge0mulc1cn  31184  rge0scvg  31192  esumcst  31322  esumpfinvallem  31333  esumpcvgval  31337  esumiun  31353  omssubadd  31558  carsggect  31576  sibfinima  31597  sitgclg  31600  sitgaddlemb  31606  eulerpartgbij  31630  rrvrnss  31705  orvcval4  31718  erdsze2lem2  32451  cvxpconn  32489  cvxsconn  32490  cvmsss2  32521  cvmliftlem8  32539  cvmlift3lem6  32571  mrsubrn  32760  msubrn  32776  mvtss  32800  mclsssvlem  32809  mclsax  32816  mclsind  32817  neibastop2lem  33708  tailfb  33725  knoppcnlem10  33841  lindsdom  34901  poimirlem2  34909  poimirlem11  34918  poimirlem19  34926  poimirlem27  34934  poimirlem30  34937  mblfinlem2  34945  itg2addnclem2  34959  itg2gt0cn  34962  ftc1anclem3  34984  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anc  34990  cnresima  35057  istotbnd3  35064  sstotbnd2  35067  totbndbnd  35082  prdsbnd  35086  cntotbnd  35089  ismtyima  35096  heibor1lem  35102  heibor  35114  rrnequiv  35128  lsatlss  36147  cdleme50rnlem  37695  cmpfiiin  39314  isnacs3  39327  eldioph2lem2  39378  fnwe2lem2  39671  lmhmfgima  39704  gneispacern  40508  imo72b2lem0  40536  imo72b2lem2  40538  imo72b2lem1  40541  imo72b2  40545  refsumcn  41307  cncmpmax  41309  elpmrn  41505  climinf  41907  climinf2lem  42007  limsupvaluz2  42039  supcnvlimsup  42041  limsupgtlem  42078  icccncfext  42190  dvsinax  42217  itgsubsticclem  42280  fourierdlem70  42481  fourierdlem82  42493  fge0npnf  42669  sge0resrnlem  42705  sge0isum  42729  sge0seq  42748  meadjiunlem  42767  omeiunle  42819  hoicvr  42850  vonvolmbllem  42962  preimaioomnf  43017  smfco  43097  mgmhmima  44089  aacllem  44922