Theorem frnd 6715

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

Syntax hints:   → wi 4   ⊆ wss 3913  ran crn 5663  ⟶wf 6533

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 210  df-an 401  df-f 6541

This theorem is referenced by:  f1un  6842  fliftrel  7307  f1iun  7940  f1dmex  7953  fo2ndf  8115  onoviun  8329  onnseq  8330  smores2  8340  domdifsn  9047  omxpenlem  9065  fodomr  9115  domss2  9123  f1domfi  9164  sucdom2  9186  f1finf1o  9232  infn0  9261  f1fi  9273  fodomfir  9286  unirnffid  9303  intrnfi  9375  dffi3  9390  ordtypelem8  9486  ordtypelem9  9487  ordtypelem10  9488  hartogslem1  9503  brwdom2  9534  unxpwdom2  9549  ixpiunwdom  9551  infdifsn  9625  cantnf  9661  ac10ct  10017  numacn  10032  infpwfien  10045  fictb  10226  isf34lem5  10361  isf34lem7  10362  isf34lem6  10363  enfin1ai  10367  canthp1lem2  10637  gch3  10660  wuncval2  10731  peano5nni  12235  hashimarn  14476  hashf1lem1  14491  hashf1lem2  14492  ccatrn  14626  swrdrn  14689  pfxrn  14722  cshwrn  14838  limsupgle  15527  limsupgre  15531  isercolllem2  15716  isercoll  15718  isercoll2  15719  climsup  15720  ruclem11  16295  4sqlem11  17014  vdwapf  17031  vdwlem11  17050  0ram  17079  funcres2b  17953  funcres2c  17959  setcepi  18144  yoniso  18340  isacs4lem  18599  chnso  18679  mgmhmima  18772  mhmima  18883  gsumwspan  18904  frmdss2  18921  cycsubm  19272  cycsubgcl  19276  cycsubgss  19277  ghmrn  19298  conjnmz  19321  ghmqusnsg  19351  ghmquskerlem3  19355  cntzmhm  19410  f1omvdconj  19515  odf1o2  19642  pgpssslw  19683  sylow2blem1  19689  lsmssv  19712  smndlsmidm  19725  pj1ghm2  19773  efgsp1  19806  efgrelexlemb  19819  cntzcmnf  19914  cyggenod  19953  gsumval3eu  19973  gsumval3lem2  19975  gsumval3  19976  gsumzsubmcl  19987  gsumzaddlem  19990  gsumzadd  19991  gsumzsplit  19996  gsumconst  20003  gsumzoppg  20013  gsumpt  20031  dmdprdd  20070  dprdfcntz  20086  dprdfeq0  20093  dprdlub  20097  dprdres  20099  dprdss  20100  dprdz  20101  subgdprd  20106  dprd2dlem1  20112  dprd2da  20113  dmdprdsplit2lem  20116  dpjghm2  20135  ablfac1b  20141  lmhmlsp  21147  pj1lmhm2  21199  pjfo  21833  frlmsplit2  21891  frlmsslsp  21914  frlmlbs  21915  frlmup3  21918  frlmup4  21919  lindff1  21938  lindfrn  21939  f1lindf  21940  indlcim  21958  aspval2  22016  mplcoe5lem  22158  mplbas2  22161  mplind  22189  evlslem1  22201  evlseu  22202  gsumply1subr  22361  m2cpmf1  22868  m2cpmghm  22869  iinopn  23027  pptbas  23133  tgrest  23284  resttopon  23286  rest0  23294  restfpw  23304  ordtbaslem  23313  ordtuni  23315  ordtbas2  23316  ordtrest  23327  ordtrest2  23329  cnclsi  23397  cnrest2r  23412  cnprest2  23415  lmss  23423  cncmp  23517  rncmp  23521  discmp  23523  connima  23550  conncn  23551  2ndcdisj  23581  2ndcomap  23583  dis2ndc  23585  lly1stc  23621  comppfsc  23657  kgencmp  23670  1stckgenlem  23678  kgencn3  23683  ptbasfi  23706  txbasval  23731  upxp  23748  uptx  23750  txtube  23765  txcmplem1  23766  txcmplem2  23767  tx1stc  23775  xkoptsub  23779  xkoco2cn  23783  xkococnlem  23784  hmeores  23896  fbasrn  24009  trfilss  24014  trfg  24016  uzrest  24022  rnelfmlem  24077  fclscmpi  24154  alexsublem  24169  ptcmplem1  24177  ptcmplem3  24179  cnextcn  24192  tmdgsum2  24221  subgtgp  24230  subgntr  24232  opnsubg  24233  clsnsg  24235  tgpconncomp  24238  tsmsfbas  24253  prdsdsf  24492  prdsxmetlem  24493  prdsmet  24495  imasdsf1olem  24498  unirnblps  24544  unirnbl  24545  prdsbl  24616  met1stc  24646  met2ndci  24647  prdsxmslem2  24654  xrge0gsumle  24959  xrge0tsms  24960  metdcn2  24965  metdsf  24974  metdsge  24975  cnmptre  25054  bndth  25085  evth  25086  evth2  25087  lebnumlem2  25089  lebnumlem3  25090  reparphti  25124  bcthlem5  25455  minveclem1  25551  minveclem3b  25555  evthicc2  25587  ovolmge0  25604  ovollb  25606  ovolgelb  25607  ovollb2lem  25615  ovollb2  25616  ovolunlem1a  25623  ovolunlem1  25624  ovoliunlem1  25629  ovoliun  25632  ovoliun2  25633  ovolscalem1  25640  ovolicc1  25643  ovolicc2lem4  25647  ovolicc2  25649  voliunlem2  25678  voliunlem3  25679  ioombl1lem2  25686  ioombl1lem4  25688  uniioovol  25706  uniiccvol  25707  uniioombllem1  25708  uniioombllem2  25710  uniioombllem3  25712  uniioombllem6  25715  uniioombl  25716  volsup2  25732  vitalilem2  25736  vitalilem4  25738  vitalilem5  25739  mbfsup  25791  mbfinf  25792  mbflimsup  25793  i1fima  25805  i1fima2  25806  itg1cl  25812  itg1ge0  25813  i1fmullem  25821  i1fadd  25822  i1fmul  25823  itg1addlem4  25826  itg1addlem5  25827  i1fmulc  25830  itg1mulc  25831  i1fres  25832  itg10a  25837  itg1ge0a  25838  itg1climres  25841  mbfi1fseqlem4  25845  itg2seq  25869  itg2monolem1  25877  itg2monolem2  25878  itg2monolem3  25879  itg2mono  25880  itg2i1fseq2  25883  itg2gt0  25887  itg2cnlem1  25888  itg2cn  25890  dvne0  26138  lhop2  26142  mdegleb  26189  mdegldg  26191  aalioulem3  26463  logccv  26793  efrlim  27099  basellem3  27212  fsumvma  27342  lgseisenlem4  27507  noseqind  28450  uhgredgn0  29418  upgredgss  29422  umgredgss  29423  edgupgr  29424  upgredg  29427  usgruspgrb  29473  upgrres1  29603  ubthlem1  31162  minvecolem1  31166  htthlem  31209  ofrn  32924  ofrn2  32925  xppreima2  32936  fsumiunle  33113  ccatws1f1olast  33212  mgcf1o  33263  gsumhashmul  33327  xrge0tsmsd  33333  symgcom  33343  cycpmcl  33376  cycpmco2lem1  33386  cycpmco2lem5  33390  cycpmco2  33393  cycpmconjv  33402  cycpmconjslem2  33415  elrgspnsubrunlem2  33508  idomsubr  33572  1arithidom  33771  psrbasfsupp  33845  esplyfv  33904  esplyfval3  33906  ply1degltdimlem  33956  cmpcref  34184  ordtrestNEW  34255  ordtrest2NEW  34257  xrge0mulc1cn  34275  rge0scvg  34283  esumcst  34397  esumpfinvallem  34408  esumpcvgval  34412  esumiun  34428  omssubadd  34634  carsggect  34652  sibfinima  34673  sitgclg  34676  sitgaddlemb  34682  eulerpartgbij  34706  rrvrnss  34781  orvcval4  34795  erdsze2lem2  35594  cvxpconn  35632  cvxsconn  35633  cvmsss2  35664  cvmliftlem8  35682  cvmlift3lem6  35714  mrsubrn  35903  msubrn  35919  mvtss  35943  mclsssvlem  35952  mclsax  35959  mclsind  35960  neibastop2lem  36759  tailfb  36776  knoppcnlem10  36979  lindsdom  38152  poimirlem2  38160  poimirlem11  38169  poimirlem19  38177  poimirlem27  38185  poimirlem30  38188  mblfinlem2  38196  itg2addnclem2  38210  itg2gt0cn  38213  ftc1anclem3  38233  ftc1anclem6  38236  ftc1anclem7  38237  ftc1anc  38239  cnresima  38302  istotbnd3  38309  sstotbnd2  38312  totbndbnd  38327  prdsbnd  38331  cntotbnd  38334  ismtyima  38341  heibor1lem  38347  heibor  38359  rrnequiv  38373  lsatlss  39659  cdleme50rnlem  41207  sticksstones2  42803  aks6d1c6lem5  42833  cmpfiiin  43319  isnacs3  43332  eldioph2lem2  43383  fnwe2lem2  43669  lmhmfgima  43702  cantnfub2  43940  onnoxpg  44046  gneispacern  44755  imo72b2lem2  44784  imo72b2lem1  44786  imo72b2  44789  refsumcn  45641  cncmpmax  45643  elpmrn  45827  climinf  46213  climinf2lem  46311  limsupvaluz2  46343  supcnvlimsup  46345  limsupgtlem  46382  icccncfext  46492  dvsinax  46518  itgsubsticclem  46580  fourierdlem70  46781  fourierdlem82  46793  fourierdlem113  46824  fge0npnf  46972  sge0resrnlem  47008  sge0isum  47032  sge0seq  47051  meadjiunlem  47070  omeiunle  47122  hoicvr  47153  vonvolmbllem  47265  preimaioomnf  47324  smfco  47407  chnsubseqwl  47486  ackvalsucsucval  49352  aacllem  50474