Theorem frnd 6663

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

Syntax hints:   → wi 4   ⊆ wss 3883  ran crn 5619  ⟶wf 6481

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 208  df-an 397  df-f 6489

This theorem is referenced by:  f1un  6787  fliftrel  7252  f1iun  7886  f1dmex  7899  fo2ndf  8060  onoviun  8273  onnseq  8274  smores2  8284  domdifsn  8988  omxpenlem  9006  fodomr  9056  domss2  9064  f1domfi  9105  sucdom2  9127  f1finf1o  9173  infn0  9202  f1fi  9214  fodomfir  9228  unirnffid  9247  intrnfi  9319  dffi3  9334  ordtypelem8  9430  ordtypelem9  9431  ordtypelem10  9432  hartogslem1  9447  brwdom2  9478  unxpwdom2  9493  ixpiunwdom  9495  infdifsn  9569  cantnf  9605  ac10ct  9947  numacn  9962  infpwfien  9975  fictb  10157  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  enfin1ai  10297  canthp1lem2  10567  gch3  10590  wuncval2  10661  peano5nni  12168  hashimarn  14393  hashf1lem1  14408  hashf1lem2  14409  ccatrn  14543  swrdrn  14606  pfxrn  14639  cshwrn  14755  limsupgle  15430  limsupgre  15434  isercolllem2  15619  isercoll  15621  isercoll2  15622  climsup  15623  ruclem11  16198  4sqlem11  16917  vdwapf  16934  vdwlem11  16953  0ram  16982  funcres2b  17855  funcres2c  17861  setcepi  18046  yoniso  18242  isacs4lem  18501  chnso  18581  mgmhmima  18674  mhmima  18784  gsumwspan  18805  frmdss2  18822  cycsubm  19168  cycsubgcl  19172  cycsubgss  19173  ghmrn  19195  conjnmz  19218  ghmqusnsg  19248  ghmquskerlem3  19252  cntzmhm  19307  f1omvdconj  19412  odf1o2  19539  pgpssslw  19580  sylow2blem1  19586  lsmssv  19609  smndlsmidm  19622  pj1ghm2  19670  efgsp1  19703  efgrelexlemb  19716  cntzcmnf  19811  cyggenod  19850  gsumval3eu  19870  gsumval3lem2  19872  gsumval3  19873  gsumzsubmcl  19884  gsumzaddlem  19887  gsumzadd  19888  gsumzsplit  19893  gsumconst  19900  gsumzoppg  19910  gsumpt  19928  dmdprdd  19967  dprdfcntz  19983  dprdfeq0  19990  dprdlub  19994  dprdres  19996  dprdss  19997  dprdz  19998  subgdprd  20003  dprd2dlem1  20009  dprd2da  20010  dmdprdsplit2lem  20013  dpjghm2  20032  ablfac1b  20038  lmhmlsp  21039  pj1lmhm2  21091  pjfo  21690  frlmsplit2  21748  frlmsslsp  21771  frlmlbs  21772  frlmup3  21775  frlmup4  21776  lindff1  21795  lindfrn  21796  f1lindf  21797  indlcim  21815  aspval2  21873  mplcoe5lem  22015  mplbas2  22018  mplind  22046  evlslem1  22058  evlseu  22059  gsumply1subr  22218  m2cpmf1  22726  m2cpmghm  22727  iinopn  22885  pptbas  22991  tgrest  23142  resttopon  23144  rest0  23152  restfpw  23162  ordtbaslem  23171  ordtuni  23173  ordtbas2  23174  ordtrest  23185  ordtrest2  23187  cnclsi  23255  cnrest2r  23270  cnprest2  23273  lmss  23281  cncmp  23375  rncmp  23379  discmp  23381  connima  23408  conncn  23409  2ndcdisj  23439  2ndcomap  23441  dis2ndc  23443  lly1stc  23479  comppfsc  23515  kgencmp  23528  1stckgenlem  23536  kgencn3  23541  ptbasfi  23564  txbasval  23589  upxp  23606  uptx  23608  txtube  23623  txcmplem1  23624  txcmplem2  23625  tx1stc  23633  xkoptsub  23637  xkoco2cn  23641  xkococnlem  23642  hmeores  23754  fbasrn  23867  trfilss  23872  trfg  23874  uzrest  23880  rnelfmlem  23935  fclscmpi  24012  alexsublem  24027  ptcmplem1  24035  ptcmplem3  24037  cnextcn  24050  tmdgsum2  24079  subgtgp  24088  subgntr  24090  opnsubg  24091  clsnsg  24093  tgpconncomp  24096  tsmsfbas  24111  prdsdsf  24350  prdsxmetlem  24351  prdsmet  24353  imasdsf1olem  24356  unirnblps  24402  unirnbl  24403  prdsbl  24474  met1stc  24504  met2ndci  24505  prdsxmslem2  24512  xrge0gsumle  24817  xrge0tsms  24818  metdcn2  24823  metdsf  24832  metdsge  24833  cnmptre  24912  bndth  24943  evth  24944  evth2  24945  lebnumlem2  24947  lebnumlem3  24948  reparphti  24982  bcthlem5  25313  minveclem1  25409  minveclem3b  25413  evthicc2  25445  ovolmge0  25462  ovollb  25464  ovolgelb  25465  ovollb2lem  25473  ovollb2  25474  ovolunlem1a  25481  ovolunlem1  25482  ovoliunlem1  25487  ovoliun  25490  ovoliun2  25491  ovolscalem1  25498  ovolicc1  25501  ovolicc2lem4  25505  ovolicc2  25507  voliunlem2  25536  voliunlem3  25537  ioombl1lem2  25544  ioombl1lem4  25546  uniioovol  25564  uniiccvol  25565  uniioombllem1  25566  uniioombllem2  25568  uniioombllem3  25570  uniioombllem6  25573  uniioombl  25574  volsup2  25590  vitalilem2  25594  vitalilem4  25596  vitalilem5  25597  mbfsup  25649  mbfinf  25650  mbflimsup  25651  i1fima  25663  i1fima2  25664  itg1cl  25670  itg1ge0  25671  i1fmullem  25679  i1fadd  25680  i1fmul  25681  itg1addlem4  25684  itg1addlem5  25685  i1fmulc  25688  itg1mulc  25689  i1fres  25690  itg10a  25695  itg1ge0a  25696  itg1climres  25699  mbfi1fseqlem4  25703  itg2seq  25727  itg2monolem1  25735  itg2monolem2  25736  itg2monolem3  25737  itg2mono  25738  itg2i1fseq2  25741  itg2gt0  25745  itg2cnlem1  25746  itg2cn  25748  dvne0  25996  lhop2  26000  mdegleb  26047  mdegldg  26049  aalioulem3  26318  logccv  26645  efrlim  26951  basellem3  27064  fsumvma  27194  lgseisenlem4  27359  noseqind  28302  uhgredgn0  29215  upgredgss  29219  umgredgss  29220  edgupgr  29221  upgredg  29224  usgruspgrb  29270  upgrres1  29400  ubthlem1  30959  minvecolem1  30963  htthlem  31006  ofrn  32731  ofrn2  32732  xppreima2  32743  fsumiunle  32921  ccatws1f1olast  33031  mgcf1o  33082  gsumhashmul  33148  xrge0tsmsd  33154  symgcom  33164  cycpmcl  33197  cycpmco2lem1  33207  cycpmco2lem5  33211  cycpmco2  33214  cycpmconjv  33223  cycpmconjslem2  33236  elrgspnsubrunlem2  33329  idomsubr  33393  1arithidom  33620  psrbasfsupp  33695  esplyfv  33754  esplyfval3  33756  ply1degltdimlem  33806  cmpcref  34034  ordtrestNEW  34105  ordtrest2NEW  34107  xrge0mulc1cn  34125  rge0scvg  34133  esumcst  34247  esumpfinvallem  34258  esumpcvgval  34262  esumiun  34278  omssubadd  34484  carsggect  34502  sibfinima  34523  sitgclg  34526  sitgaddlemb  34532  eulerpartgbij  34556  rrvrnss  34631  orvcval4  34645  erdsze2lem2  35432  cvxpconn  35470  cvxsconn  35471  cvmsss2  35502  cvmliftlem8  35520  cvmlift3lem6  35552  mrsubrn  35741  msubrn  35757  mvtss  35781  mclsssvlem  35790  mclsax  35797  mclsind  35798  neibastop2lem  36588  tailfb  36605  knoppcnlem10  36808  lindsdom  37981  poimirlem2  37989  poimirlem11  37998  poimirlem19  38006  poimirlem27  38014  poimirlem30  38017  mblfinlem2  38025  itg2addnclem2  38039  itg2gt0cn  38042  ftc1anclem3  38062  ftc1anclem6  38065  ftc1anclem7  38066  ftc1anc  38068  cnresima  38131  istotbnd3  38138  sstotbnd2  38141  totbndbnd  38156  prdsbnd  38160  cntotbnd  38163  ismtyima  38170  heibor1lem  38176  heibor  38188  rrnequiv  38202  lsatlss  39488  cdleme50rnlem  41036  sticksstones2  42632  aks6d1c6lem5  42662  cmpfiiin  43146  isnacs3  43159  eldioph2lem2  43210  fnwe2lem2  43496  lmhmfgima  43529  cantnfub2  43767  onnoxpg  43873  gneispacern  44582  imo72b2lem2  44611  imo72b2lem1  44613  imo72b2  44616  refsumcn  45478  cncmpmax  45480  elpmrn  45665  climinf  46051  climinf2lem  46149  limsupvaluz2  46181  supcnvlimsup  46183  limsupgtlem  46220  icccncfext  46330  dvsinax  46356  itgsubsticclem  46418  fourierdlem70  46619  fourierdlem82  46631  fge0npnf  46810  sge0resrnlem  46846  sge0isum  46870  sge0seq  46889  meadjiunlem  46908  omeiunle  46960  hoicvr  46991  vonvolmbllem  47103  preimaioomnf  47162  smfco  47245  chnsubseqwl  47324  ackvalsucsucval  49179  aacllem  50291