Theorem frnd 6718

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3906  ran crn 5664  ⟶wf 6536

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 6544

This theorem is used by:  f1un  6845  fliftrel  7315  f1iun  7947  f1dmex  7960  fo2ndf  8122  onoviun  8336  onnseq  8337  smores2  8347  domdifsn  9055  omxpenlem  9073  fodomr  9123  domss2  9131  f1domfi  9172  sucdom2  9194  f1finf1o  9240  infn0  9269  f1fi  9281  fodomfir  9294  unirnffid  9311  intrnfi  9383  dffi3  9398  ordtypelem8  9494  ordtypelem9  9495  ordtypelem10  9496  hartogslem1  9511  brwdom2  9542  unxpwdom2  9557  ixpiunwdom  9559  infdifsn  9633  cantnf  9669  numacn  10049  infpwfien  10062  fictb  10243  isf34lem5  10377  isf34lem7  10378  isf34lem6  10379  enfin1ai  10383  canthp1lem2  10655  gch3  10678  wuncval2  10749  peano5nni  12253  hashimarn  14497  hashf1lem1  14512  hashf1lem2  14513  ccatrn  14647  swrdrn  14713  pfxrn  14747  cshwrn  14865  limsupgle  15554  limsupgre  15558  isercolllem2  15743  isercoll  15745  isercoll2  15746  climsup  15747  ruclem11  16320  4sqlem11  17039  vdwapf  17056  vdwlem11  17075  0ram  17104  funcres2b  17978  funcres2c  17984  setcepi  18169  yoniso  18365  isacs4lem  18624  chnso  18704  mgmhmima  18807  mhmima  18923  gsumwspan  18944  frmdss2  18961  cycsubm  19319  cycsubgcl  19323  cycsubgss  19324  ghmrn  19345  conjnmz  19368  ghmqusnsg  19398  ghmquskerlem3  19402  cntzmhm  19457  f1omvdconj  19562  odf1o2  19689  pgpssslw  19730  sylow2blem1  19736  lsmssv  19759  smndlsmidm  19772  pj1ghm2  19820  efgsp1  19853  efgrelexlemb  19866  cntzcmnf  19961  cyggenod  20000  gsumval3eu  20020  gsumval3lem2  20022  gsumval3  20023  gsumzsubmcl  20034  gsumzaddlem  20037  gsumzadd  20038  gsumzsplit  20043  gsumconst  20050  gsumzoppg  20060  gsumpt  20078  dmdprdd  20117  dprdfcntz  20133  dprdfeq0  20140  dprdlub  20144  dprdres  20146  dprdss  20147  dprdz  20148  subgdprd  20153  dprd2dlem1  20159  dprd2da  20160  dmdprdsplit2lem  20163  dpjghm2  20182  ablfac1b  20188  lmhmlsp  21222  pj1lmhm2  21274  pjfo  21917  frlmsplit2  21975  frlmsslsp  21998  frlmlbs  21999  frlmup3  22002  frlmup4  22003  lindff1  22022  lindfrn  22023  f1lindf  22024  indlcim  22042  aspval2  22100  mplcoe5lem  22242  mplbas2  22245  mplind  22273  evlslem1  22285  evlseu  22286  gsumply1subr  22445  m2cpmf1  22952  m2cpmghm  22953  iinopn  23111  pptbas  23217  tgrest  23368  resttopon  23370  rest0  23378  restfpw  23388  ordtbaslem  23397  ordtuni  23399  ordtbas2  23400  ordtrest  23411  ordtrest2  23413  cnclsi  23481  cnrest2r  23496  cnprest2  23499  lmss  23507  cncmp  23601  rncmp  23605  discmp  23607  connima  23634  conncn  23635  2ndcdisj  23666  2ndcomap  23668  dis2ndc  23670  lly1stc  23706  comppfsc  23742  kgencmp  23755  1stckgenlem  23763  kgencn3  23768  ptbasfi  23791  txbasval  23816  upxp  23833  uptx  23835  txtube  23850  txcmplem1  23851  txcmplem2  23852  tx1stc  23860  xkoptsub  23864  xkoco2cn  23868  xkococnlem  23869  hmeores  23981  fbasrn  24094  trfilss  24099  trfg  24101  uzrest  24107  rnelfmlem  24162  fclscmpi  24239  alexsublem  24254  ptcmplem1  24262  ptcmplem3  24264  cnextcn  24277  tmdgsum2  24306  subgtgp  24315  subgntr  24317  opnsubg  24318  clsnsg  24320  tgpconncomp  24323  tsmsfbas  24338  prdsdsf  24577  prdsxmetlem  24578  prdsmet  24580  imasdsf1olem  24583  unirnblps  24629  unirnbl  24630  prdsbl  24701  met1stc  24731  met2ndci  24732  prdsxmslem2  24739  xrge0gsumle  25044  xrge0tsms  25045  metdcn2  25050  metdsf  25059  metdsge  25060  cnmptre  25139  bndth  25170  evth  25171  evth2  25172  lebnumlem2  25174  lebnumlem3  25175  reparphti  25209  bcthlem5  25540  minveclem1  25636  minveclem3b  25640  evthicc2  25672  ovolmge0  25689  ovollb  25691  ovolgelb  25692  ovollb2lem  25700  ovollb2  25701  ovolunlem1a  25708  ovolunlem1  25709  ovoliunlem1  25714  ovoliun  25717  ovoliun2  25718  ovolscalem1  25725  ovolicc1  25728  ovolicc2lem4  25732  ovolicc2  25734  voliunlem2  25763  voliunlem3  25764  ioombl1lem2  25771  ioombl1lem4  25773  uniioovol  25791  uniiccvol  25792  uniioombllem1  25793  uniioombllem2  25795  uniioombllem3  25797  uniioombllem6  25800  uniioombl  25801  volsup2  25817  vitalilem2  25821  vitalilem4  25823  vitalilem5  25824  mbfsup  25876  mbfinf  25877  mbflimsup  25878  i1fima  25890  i1fima2  25891  itg1cl  25897  itg1ge0  25898  i1fmullem  25906  i1fadd  25907  i1fmul  25908  itg1addlem4  25911  itg1addlem5  25912  i1fmulc  25915  itg1mulc  25916  i1fres  25917  itg10a  25922  itg1ge0a  25923  itg1climres  25926  mbfi1fseqlem4  25930  itg2seq  25954  itg2monolem1  25962  itg2monolem2  25963  itg2monolem3  25964  itg2mono  25965  itg2i1fseq2  25968  itg2gt0  25972  itg2cnlem1  25973  itg2cn  25975  dvne0  26223  lhop2  26227  mdegleb  26274  mdegldg  26276  aalioulem3  26550  logccv  26881  efrlim  27187  basellem3  27300  fsumvma  27430  lgseisenlem4  27595  noseqind  28538  uhgredgn0  29535  upgredgss  29539  umgredgss  29540  edgupgr  29541  upgredg  29544  usgruspgrb  29593  upgrres1  29723  ubthlem1  31295  minvecolem1  31299  htthlem  31342  ofrn  33057  ofrn2  33058  xppreima2  33069  fsumiunle  33245  ccatws1f1olast  33340  mgcf1o  33389  gsumhashmul  33453  xrge0tsmsd  33459  symgcom  33469  cycpmcl  33502  cycpmco2lem1  33512  cycpmco2lem5  33516  cycpmco2  33519  cycpmconjv  33528  cycpmconjslem2  33541  elrgspnsubrunlem2  33634  idomsubr  33696  1arithidom  33893  psrbasfsupp  33967  esplyfv  34026  esplyfval3  34028  ply1degltdimlem  34078  cmpcref  34306  ordtrestNEW  34377  ordtrest2NEW  34379  xrge0mulc1cn  34397  rge0scvg  34405  esumcst  34519  esumpfinvallem  34530  esumpcvgval  34534  esumiun  34550  omssubadd  34757  carsggect  34775  sibfinima  34796  sitgclg  34799  sitgaddlemb  34805  eulerpartgbij  34829  rrvrnss  34904  orvcval4  34918  erdsze2lem2  35735  cvxpconn  35773  cvxsconn  35774  cvmsss2  35805  cvmliftlem8  35823  cvmlift3lem6  35855  mrsubrn  36044  msubrn  36060  mvtss  36084  mclsssvlem  36093  mclsax  36100  mclsind  36101  neibastop2lem  36930  tailfb  36947  knoppcnlem10  37150  lindsdom  38324  poimirlem2  38332  poimirlem11  38341  poimirlem19  38349  poimirlem27  38357  poimirlem30  38360  mblfinlem2  38368  itg2addnclem2  38382  itg2gt0cn  38385  ftc1anclem3  38405  ftc1anclem6  38408  ftc1anclem7  38409  ftc1anc  38411  cnresima  38475  istotbnd3  38482  sstotbnd2  38485  totbndbnd  38500  prdsbnd  38504  cntotbnd  38507  ismtyima  38514  heibor1lem  38520  heibor  38532  rrnequiv  38546  lsatlss  39830  cdleme50rnlem  41378  sticksstones2  42974  aks6d1c6lem5  43004  cmpfiiin  43488  isnacs3  43501  eldioph2lem2  43552  fnwe2lem2  43838  lmhmfgima  43871  cantnfub2  44109  onnoxpg  44215  gneispacern  44924  imo72b2lem2  44953  imo72b2lem1  44955  imo72b2  44958  refsumcn  45810  cncmpmax  45812  elpmrn  45996  climinf  46382  climinf2lem  46480  limsupvaluz2  46512  supcnvlimsup  46514  limsupgtlem  46551  icccncfext  46661  dvsinax  46687  itgsubsticclem  46749  fourierdlem70  46950  fourierdlem82  46962  fourierdlem113  46993  fge0npnf  47141  sge0resrnlem  47177  sge0isum  47201  sge0seq  47220  meadjiunlem  47239  omeiunle  47291  hoicvr  47322  vonvolmbllem  47434  preimaioomnf  47493  smfco  47576  chnsubseqwl  47655  ackvalsucsucval  49527  aacllem  50680