Theorem frnd 6748

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  ran crn 5659  ⟶wf 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6570

This theorem is used by:  f1un  6875  fliftrel  7347  f1iun  7990  f1dmex  8003  fo2ndf  8169  onoviun  8389  onnseq  8390  smores2  8400  domdifsn  9117  omxpenlem  9135  fodomr  9185  domss2  9193  f1domfi  9234  sucdom2  9256  f1finf1o  9302  infn0  9332  f1fi  9344  fodomfir  9357  unirnffid  9374  intrnfi  9445  dffi3  9460  ordtypelem8  9556  ordtypelem9  9557  ordtypelem10  9558  hartogslem1  9573  brwdom2  9604  unxpwdom2  9619  ixpiunwdom  9621  infdifsn  9695  cantnf  9731  numacn  10167  infpwfien  10180  fictb  10361  isf34lem5  10495  isf34lem7  10496  isf34lem6  10497  enfin1ai  10501  canthp1lem2  10777  gch3  10800  wuncval2  10871  peano5nni  12378  hashimarn  14626  hashf1lem1  14641  hashf1lem2  14642  ccatrn  14776  swrdrn  14843  pfxrn  14877  cshwrn  14995  limsupgle  15688  limsupgre  15692  isercolllem2  15877  isercoll  15879  isercoll2  15880  climsup  15881  ruclem11  16452  4sqlem11  17177  vdwapf  17194  vdwlem11  17213  0ram  17242  funcres2b  18122  funcres2c  18128  setcepi  18313  yoniso  18509  isacs4lem  18768  chnso  18848  mgmhmima  18954  mhmima  19071  gsumwspan  19092  frmdss2  19109  cycsubm  19467  cycsubgcl  19471  cycsubgss  19472  ghmrn  19493  conjnmz  19516  ghmqusnsg  19547  ghmquskerlem3  19551  cntzmhm  19606  f1omvdconj  19711  odf1o2  19838  pgpssslw  19879  sylow2blem1  19885  lsmssv  19908  smndlsmidm  19921  pj1ghm2  19969  efgsp1  20002  efgrelexlemb  20015  cntzcmnf  20110  cyggenod  20149  gsumval3eu  20169  gsumval3lem2  20171  gsumval3  20172  gsumzsubmcl  20183  gsumzaddlem  20186  gsumzadd  20187  gsumzsplit  20192  gsumconst  20199  gsumzoppg  20209  gsumpt  20227  dmdprdd  20266  dprdfcntz  20282  dprdfeq0  20289  dprdlub  20293  dprdres  20295  dprdss  20296  dprdz  20297  subgdprd  20302  dprd2dlem1  20308  dprd2da  20309  dmdprdsplit2lem  20312  dpjghm2  20331  ablfac1b  20337  lmhmlsp  21375  pj1lmhm2  21427  pjfo  22076  frlmsplit2  22134  frlmsslsp  22157  frlmlbs  22158  frlmup3  22161  frlmup4  22162  lindff1  22181  lindfrn  22182  f1lindf  22183  indlcim  22201  lindsdom  22211  aspval2  22261  mplcoe5lem  22403  mplbas2  22406  mplind  22434  evlslem1  22446  evlseu  22447  gsumply1subr  22606  m2cpmf1  23116  m2cpmghm  23117  iinopn  23275  pptbas  23381  tgrest  23532  resttopon  23534  rest0  23542  restfpw  23552  ordtbaslem  23561  ordtuni  23563  ordtbas2  23564  ordtrest  23575  ordtrest2  23577  cnclsi  23645  cnrest2r  23660  cnprest2  23663  lmss  23671  cncmp  23765  rncmp  23769  discmp  23771  connima  23798  conncn  23799  2ndcdisj  23830  2ndcomap  23832  dis2ndc  23834  lly1stc  23870  comppfsc  23906  kgencmp  23919  1stckgenlem  23927  kgencn3  23932  ptbasfi  23955  txbasval  23980  upxp  23997  uptx  23999  txtube  24014  txcmplem1  24015  txcmplem2  24016  tx1stc  24024  xkoptsub  24028  xkoco2cn  24032  xkococnlem  24033  hmeores  24145  fbasrn  24258  trfilss  24263  trfg  24265  uzrest  24271  rnelfmlem  24326  fclscmpi  24403  alexsublem  24418  ptcmplem1  24426  ptcmplem3  24428  cnextcn  24441  tmdgsum2  24470  subgtgp  24479  subgntr  24481  opnsubg  24482  clsnsg  24484  tgpconncomp  24487  tsmsfbas  24502  prdsdsf  24741  prdsxmetlem  24742  prdsmet  24744  imasdsf1olem  24747  unirnblps  24793  unirnbl  24794  prdsbl  24865  met1stc  24895  met2ndci  24896  prdsxmslem2  24903  xrge0gsumle  25208  xrge0tsms  25209  metdcn2  25214  metdsf  25223  metdsge  25224  cnmptre  25303  bndth  25334  evth  25335  evth2  25336  lebnumlem2  25338  lebnumlem3  25339  reparphti  25373  bcthlem5  25704  minveclem1  25800  minveclem3b  25804  evthicc2  25836  ovolmge0  25853  ovollb  25855  ovolgelb  25856  ovollb2lem  25864  ovollb2  25865  ovolunlem1a  25872  ovolunlem1  25873  ovoliunlem1  25878  ovoliun  25881  ovoliun2  25882  ovolscalem1  25889  ovolicc1  25892  ovolicc2lem4  25896  ovolicc2  25898  voliunlem2  25927  voliunlem3  25928  ioombl1lem2  25935  ioombl1lem4  25937  uniioovol  25955  uniiccvol  25956  uniioombllem1  25957  uniioombllem2  25959  uniioombllem3  25961  uniioombllem6  25964  uniioombl  25965  volsup2  25981  vitalilem2  25985  vitalilem4  25987  vitalilem5  25988  mbfsup  26040  mbfinf  26041  mbflimsup  26042  i1fima  26054  i1fima2  26055  itg1cl  26061  itg1ge0  26062  i1fmullem  26070  i1fadd  26071  i1fmul  26072  itg1addlem4  26075  itg1addlem5  26076  i1fmulc  26079  itg1mulc  26080  i1fres  26081  itg10a  26086  itg1ge0a  26087  itg1climres  26090  mbfi1fseqlem4  26094  itg2seq  26118  itg2monolem1  26126  itg2monolem2  26127  itg2monolem3  26128  itg2mono  26129  itg2i1fseq2  26132  itg2gt0  26136  itg2cnlem1  26137  itg2cn  26139  dvne0  26386  lhop2  26390  mdegleb  26437  mdegldg  26439  rnplynfin  26685  plyconz  26686  aalioulem3  26718  logccv  27048  efrlim  27354  basellem3  27467  fsumvma  27597  lgseisenlem4  27762  noseqind  28735  uhgredgn0  29763  upgredgss  29767  umgredgss  29768  edgupgr  29769  upgredg  29772  usgruspgrb  29821  upgrres1  29951  ubthlem1  31529  minvecolem1  31533  htthlem  31576  ofrn  33331  ofrn2  33332  xppreima2  33343  fsumiunle  33516  ccatws1f1olast  33611  mgcf1o  33663  gsumhashmul  33727  xrge0tsmsd  33733  symgcom  33743  cycpmcl  33776  cycpmco2lem1  33786  cycpmco2lem5  33790  cycpmco2  33793  cycpmconjv  33802  cycpmconjslem2  33815  elrgspnsubrunlem2  33908  idomsubr  33975  1arithidom  34173  psrbasfsupp  34254  esplyfv  34313  esplyfval3  34315  ply1degltdimlem  34365  cmpcref  34593  ordtrestNEW  34664  ordtrest2NEW  34666  xrge0mulc1cn  34684  rge0scvg  34692  esumcst  34806  esumpfinvallem  34817  esumpcvgval  34821  esumiun  34837  omssubadd  35043  carsggect  35061  sibfinima  35082  sitgclg  35085  sitgaddlemb  35091  eulerpartgbij  35115  rrvrnss  35190  orvcval4  35204  onf1we  35844  onprcf1acwevd  36088  erdsze2lem2  36177  cvxpconn  36215  cvxsconn  36216  cvmsss2  36247  cvmliftlem8  36265  cvmlift3lem6  36297  mrsubrn  36486  msubrn  36502  mvtss  36526  mclsssvlem  36535  mclsax  36542  mclsind  36543  neibastop2lem  37363  tailfb  37380  knoppcnlem10  37583  pibt2  38608  poimirlem2  38808  poimirlem11  38817  poimirlem19  38825  poimirlem27  38833  poimirlem30  38836  mblfinlem2  38844  itg2addnclem2  38858  itg2gt0cn  38861  ftc1anclem3  38881  ftc1anclem6  38884  ftc1anclem7  38885  ftc1anc  38887  cnresima  38964  istotbnd3  38971  sstotbnd2  38974  totbndbnd  38989  prdsbnd  38993  cntotbnd  38996  ismtyima  39003  heibor1lem  39009  heibor  39021  rrnequiv  39035  lsatlss  40319  cdleme50rnlem  41867  sticksstones2  43463  aks6d1c6lem5  43493  cmpfiiin  43974  isnacs3  43987  eldioph2lem2  44038  lmhmfgima  44352  cantnfub2  44585  onnoxpg  44691  gneispacern  45399  imo72b2lem2  45428  imo72b2lem1  45430  imo72b2  45433  refsumcn  46321  cncmpmax  46323  elpmrn  46506  climinf  46891  climinf2lem  46989  limsupvaluz2  47021  supcnvlimsup  47023  limsupgtlem  47060  icccncfext  47170  dvsinax  47196  itgsubsticclem  47258  fourierdlem70  47459  fourierdlem82  47471  fourierdlem113  47502  fge0npnf  47650  sge0resrnlem  47686  sge0isum  47710  sge0seq  47729  meadjiunlem  47748  omeiunle  47800  hoicvr  47831  vonvolmbllem  47943  preimaioomnf  48002  smfco  48085  chnsubseqwl  48162  tmachlem-fssscan  48233  ackvalsucsucval  50131  aacllem  51367