Theorem frnd 6592

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

Syntax hints:   → wi 4   ⊆ wss 3883  ran crn 5581  ⟶wf 6414

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 396  df-f 6422

This theorem is referenced by:  fliftrel  7159  f1iun  7760  f1dmex  7773  fo2ndf  7933  onoviun  8145  onnseq  8146  smores2  8156  domdifsn  8795  omxpenlem  8813  sucdom2  8822  fodomr  8864  domss2  8872  f1domfi  8928  f1finf1o  8975  f1fi  9036  unirnffid  9041  intrnfi  9105  dffi3  9120  ordtypelem8  9214  ordtypelem9  9215  ordtypelem10  9216  hartogslem1  9231  brwdom2  9262  unxpwdom2  9277  ixpiunwdom  9279  infdifsn  9345  cantnf  9381  ac10ct  9721  numacn  9736  infpwfien  9749  fictb  9932  isf34lem5  10065  isf34lem7  10066  isf34lem6  10067  enfin1ai  10071  canthp1lem2  10340  gch3  10363  wuncval2  10434  peano5nni  11906  hashimarn  14083  hashf1lem1  14096  hashf1lem1OLD  14097  hashf1lem2  14098  ccatrn  14222  swrdrn  14293  pfxrn  14326  cshwrn  14443  limsupgle  15114  limsupgre  15118  isercolllem2  15305  isercoll  15307  isercoll2  15308  climsup  15309  ruclem11  15877  4sqlem11  16584  vdwapf  16601  vdwlem11  16620  0ram  16649  funcres2b  17528  funcres2c  17533  setcepi  17719  yoniso  17919  isacs4lem  18177  mhmima  18378  gsumwspan  18400  frmdss2  18417  cycsubm  18736  cycsubgcl  18740  cycsubgss  18741  ghmrn  18762  conjnmz  18783  cntzmhm  18860  f1omvdconj  18969  odf1o2  19093  pgpssslw  19134  sylow2blem1  19140  lsmssv  19163  smndlsmidm  19176  lsmidmOLD  19184  pj1ghm2  19225  efgsp1  19258  efgrelexlemb  19271  cntzcmnf  19361  cyggenod  19399  gsumval3eu  19420  gsumval3lem2  19422  gsumval3  19423  gsumzsubmcl  19434  gsumzaddlem  19437  gsumzadd  19438  gsumzsplit  19443  gsumconst  19450  gsumzoppg  19460  gsumpt  19478  dmdprdd  19517  dprdfcntz  19533  dprdfeq0  19540  dprdlub  19544  dprdres  19546  dprdss  19547  dprdz  19548  subgdprd  19553  dprd2dlem1  19559  dprd2da  19560  dmdprdsplit2lem  19563  dpjghm2  19582  ablfac1b  19588  lmhmlsp  20226  pj1lmhm2  20278  pjfo  20832  frlmsplit2  20890  frlmsslsp  20913  frlmlbs  20914  frlmup3  20917  frlmup4  20918  lindff1  20937  lindfrn  20938  f1lindf  20939  indlcim  20957  aspval2  21012  mplcoe5lem  21150  mplbas2  21153  mplind  21188  evlslem1  21202  evlseu  21203  gsumply1subr  21315  m2cpmf1  21800  m2cpmghm  21801  iinopn  21959  pptbas  22066  tgrest  22218  resttopon  22220  rest0  22228  restfpw  22238  ordtbaslem  22247  ordtuni  22249  ordtbas2  22250  ordtrest  22261  ordtrest2  22263  cnclsi  22331  cnrest2r  22346  cnprest2  22349  lmss  22357  cncmp  22451  rncmp  22455  discmp  22457  connima  22484  conncn  22485  2ndcdisj  22515  2ndcomap  22517  dis2ndc  22519  lly1stc  22555  comppfsc  22591  kgencmp  22604  1stckgenlem  22612  kgencn3  22617  ptbasfi  22640  txbasval  22665  upxp  22682  uptx  22684  txtube  22699  txcmplem1  22700  txcmplem2  22701  tx1stc  22709  xkoptsub  22713  xkoco2cn  22717  xkococnlem  22718  hmeores  22830  fbasrn  22943  trfilss  22948  trfg  22950  uzrest  22956  rnelfmlem  23011  fclscmpi  23088  alexsublem  23103  ptcmplem1  23111  ptcmplem3  23113  cnextcn  23126  tmdgsum2  23155  subgtgp  23164  subgntr  23166  opnsubg  23167  clsnsg  23169  tgpconncomp  23172  tsmsfbas  23187  prdsdsf  23428  prdsxmetlem  23429  prdsmet  23431  imasdsf1olem  23434  unirnblps  23480  unirnbl  23481  prdsbl  23553  met1stc  23583  met2ndci  23584  prdsxmslem2  23591  xrge0gsumle  23902  xrge0tsms  23903  metdcn2  23908  metdsf  23917  metdsge  23918  cnmptre  23996  bndth  24027  evth  24028  evth2  24029  lebnumlem2  24031  lebnumlem3  24032  reparphti  24066  bcthlem5  24397  minveclem1  24493  minveclem3b  24497  evthicc2  24529  ovolmge0  24546  ovollb  24548  ovolgelb  24549  ovollb2lem  24557  ovollb2  24558  ovolunlem1a  24565  ovolunlem1  24566  ovoliunlem1  24571  ovoliun  24574  ovoliun2  24575  ovolscalem1  24582  ovolicc1  24585  ovolicc2lem4  24589  ovolicc2  24591  voliunlem2  24620  voliunlem3  24621  ioombl1lem2  24628  ioombl1lem4  24630  uniioovol  24648  uniiccvol  24649  uniioombllem1  24650  uniioombllem2  24652  uniioombllem3  24654  uniioombllem6  24657  uniioombl  24658  volsup2  24674  vitalilem2  24678  vitalilem4  24680  vitalilem5  24681  mbfsup  24733  mbfinf  24734  mbflimsup  24735  i1fima  24747  i1fima2  24748  itg1cl  24754  itg1ge0  24755  i1fmullem  24763  i1fadd  24764  i1fmul  24765  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  i1fmulc  24773  itg1mulc  24774  i1fres  24775  itg10a  24780  itg1ge0a  24781  itg1climres  24784  mbfi1fseqlem4  24788  itg2seq  24812  itg2monolem1  24820  itg2monolem2  24821  itg2monolem3  24822  itg2mono  24823  itg2i1fseq2  24826  itg2gt0  24830  itg2cnlem1  24831  itg2cn  24833  dvne0  25080  lhop2  25084  mdegleb  25134  mdegldg  25136  aalioulem3  25399  logccv  25723  efrlim  26024  basellem3  26137  fsumvma  26266  lgseisenlem4  26431  uhgredgn0  27401  upgredgss  27405  umgredgss  27406  edgupgr  27407  upgredg  27410  usgruspgrb  27454  upgrres1  27583  ubthlem1  29133  minvecolem1  29137  htthlem  29180  ofrn  30877  ofrn2  30878  xppreima2  30889  fsumiunle  31045  mgcf1o  31183  gsumhashmul  31218  xrge0tsmsd  31219  symgcom  31254  cycpmcl  31285  cycpmco2lem1  31295  cycpmco2lem5  31299  cycpmco2  31302  cycpmconjv  31311  cycpmconjslem2  31324  cmpcref  31702  ordtrestNEW  31773  ordtrest2NEW  31775  xrge0mulc1cn  31793  rge0scvg  31801  esumcst  31931  esumpfinvallem  31942  esumpcvgval  31946  esumiun  31962  omssubadd  32167  carsggect  32185  sibfinima  32206  sitgclg  32209  sitgaddlemb  32215  eulerpartgbij  32239  rrvrnss  32314  orvcval4  32327  erdsze2lem2  33066  cvxpconn  33104  cvxsconn  33105  cvmsss2  33136  cvmliftlem8  33154  cvmlift3lem6  33186  mrsubrn  33375  msubrn  33391  mvtss  33415  mclsssvlem  33424  mclsax  33431  mclsind  33432  neibastop2lem  34476  tailfb  34493  knoppcnlem10  34609  lindsdom  35698  poimirlem2  35706  poimirlem11  35715  poimirlem19  35723  poimirlem27  35731  poimirlem30  35734  mblfinlem2  35742  itg2addnclem2  35756  itg2gt0cn  35759  ftc1anclem3  35779  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anc  35785  cnresima  35849  istotbnd3  35856  sstotbnd2  35859  totbndbnd  35874  prdsbnd  35878  cntotbnd  35881  ismtyima  35888  heibor1lem  35894  heibor  35906  rrnequiv  35920  lsatlss  36937  cdleme50rnlem  38485  sticksstones2  40031  cmpfiiin  40435  isnacs3  40448  eldioph2lem2  40499  fnwe2lem2  40792  lmhmfgima  40825  gneispacern  41637  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2lem1  41669  imo72b2  41672  refsumcn  42462  cncmpmax  42464  elpmrn  42649  climinf  43037  climinf2lem  43137  limsupvaluz2  43169  supcnvlimsup  43171  limsupgtlem  43208  icccncfext  43318  dvsinax  43344  itgsubsticclem  43406  fourierdlem70  43607  fourierdlem82  43619  fge0npnf  43795  sge0resrnlem  43831  sge0isum  43855  sge0seq  43874  meadjiunlem  43893  omeiunle  43945  hoicvr  43976  vonvolmbllem  44088  preimaioomnf  44143  smfco  44223  mgmhmima  45244  ackvalsucsucval  45922  aacllem  46391