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  7941  f1dmex  7954  fo2ndf  8116  onoviun  8330  onnseq  8331  smores2  8341  domdifsn  9048  omxpenlem  9066  fodomr  9116  domss2  9124  f1domfi  9165  sucdom2  9187  f1finf1o  9233  infn0  9262  f1fi  9274  fodomfir  9287  unirnffid  9304  intrnfi  9376  dffi3  9391  ordtypelem8  9487  ordtypelem9  9488  ordtypelem10  9489  hartogslem1  9504  brwdom2  9535  unxpwdom2  9550  ixpiunwdom  9552  infdifsn  9626  cantnf  9662  ac10ct  10018  numacn  10033  infpwfien  10046  fictb  10227  isf34lem5  10362  isf34lem7  10363  isf34lem6  10364  enfin1ai  10368  canthp1lem2  10638  gch3  10661  wuncval2  10732  peano5nni  12236  hashimarn  14477  hashf1lem1  14492  hashf1lem2  14493  ccatrn  14627  swrdrn  14690  pfxrn  14723  cshwrn  14839  limsupgle  15528  limsupgre  15532  isercolllem2  15717  isercoll  15719  isercoll2  15720  climsup  15721  ruclem11  16296  4sqlem11  17015  vdwapf  17032  vdwlem11  17051  0ram  17080  funcres2b  17954  funcres2c  17960  setcepi  18145  yoniso  18341  isacs4lem  18600  chnso  18680  mgmhmima  18773  mhmima  18884  gsumwspan  18905  frmdss2  18922  cycsubm  19273  cycsubgcl  19277  cycsubgss  19278  ghmrn  19299  conjnmz  19322  ghmqusnsg  19352  ghmquskerlem3  19356  cntzmhm  19411  f1omvdconj  19516  odf1o2  19643  pgpssslw  19684  sylow2blem1  19690  lsmssv  19713  smndlsmidm  19726  pj1ghm2  19774  efgsp1  19807  efgrelexlemb  19820  cntzcmnf  19915  cyggenod  19954  gsumval3eu  19974  gsumval3lem2  19976  gsumval3  19977  gsumzsubmcl  19988  gsumzaddlem  19991  gsumzadd  19992  gsumzsplit  19997  gsumconst  20004  gsumzoppg  20014  gsumpt  20032  dmdprdd  20071  dprdfcntz  20087  dprdfeq0  20094  dprdlub  20098  dprdres  20100  dprdss  20101  dprdz  20102  subgdprd  20107  dprd2dlem1  20113  dprd2da  20114  dmdprdsplit2lem  20117  dpjghm2  20136  ablfac1b  20142  lmhmlsp  21148  pj1lmhm2  21200  pjfo  21834  frlmsplit2  21892  frlmsslsp  21915  frlmlbs  21916  frlmup3  21919  frlmup4  21920  lindff1  21939  lindfrn  21940  f1lindf  21941  indlcim  21959  aspval2  22017  mplcoe5lem  22159  mplbas2  22162  mplind  22190  evlslem1  22202  evlseu  22203  gsumply1subr  22362  m2cpmf1  22869  m2cpmghm  22870  iinopn  23028  pptbas  23134  tgrest  23285  resttopon  23287  rest0  23295  restfpw  23305  ordtbaslem  23314  ordtuni  23316  ordtbas2  23317  ordtrest  23328  ordtrest2  23330  cnclsi  23398  cnrest2r  23413  cnprest2  23416  lmss  23424  cncmp  23518  rncmp  23522  discmp  23524  connima  23551  conncn  23552  2ndcdisj  23582  2ndcomap  23584  dis2ndc  23586  lly1stc  23622  comppfsc  23658  kgencmp  23671  1stckgenlem  23679  kgencn3  23684  ptbasfi  23707  txbasval  23732  upxp  23749  uptx  23751  txtube  23766  txcmplem1  23767  txcmplem2  23768  tx1stc  23776  xkoptsub  23780  xkoco2cn  23784  xkococnlem  23785  hmeores  23897  fbasrn  24010  trfilss  24015  trfg  24017  uzrest  24023  rnelfmlem  24078  fclscmpi  24155  alexsublem  24170  ptcmplem1  24178  ptcmplem3  24180  cnextcn  24193  tmdgsum2  24222  subgtgp  24231  subgntr  24233  opnsubg  24234  clsnsg  24236  tgpconncomp  24239  tsmsfbas  24254  prdsdsf  24493  prdsxmetlem  24494  prdsmet  24496  imasdsf1olem  24499  unirnblps  24545  unirnbl  24546  prdsbl  24617  met1stc  24647  met2ndci  24648  prdsxmslem2  24655  xrge0gsumle  24960  xrge0tsms  24961  metdcn2  24966  metdsf  24975  metdsge  24976  cnmptre  25055  bndth  25086  evth  25087  evth2  25088  lebnumlem2  25090  lebnumlem3  25091  reparphti  25125  bcthlem5  25456  minveclem1  25552  minveclem3b  25556  evthicc2  25588  ovolmge0  25605  ovollb  25607  ovolgelb  25608  ovollb2lem  25616  ovollb2  25617  ovolunlem1a  25624  ovolunlem1  25625  ovoliunlem1  25630  ovoliun  25633  ovoliun2  25634  ovolscalem1  25641  ovolicc1  25644  ovolicc2lem4  25648  ovolicc2  25650  voliunlem2  25679  voliunlem3  25680  ioombl1lem2  25687  ioombl1lem4  25689  uniioovol  25707  uniiccvol  25708  uniioombllem1  25709  uniioombllem2  25711  uniioombllem3  25713  uniioombllem6  25716  uniioombl  25717  volsup2  25733  vitalilem2  25737  vitalilem4  25739  vitalilem5  25740  mbfsup  25792  mbfinf  25793  mbflimsup  25794  i1fima  25806  i1fima2  25807  itg1cl  25813  itg1ge0  25814  i1fmullem  25822  i1fadd  25823  i1fmul  25824  itg1addlem4  25827  itg1addlem5  25828  i1fmulc  25831  itg1mulc  25832  i1fres  25833  itg10a  25838  itg1ge0a  25839  itg1climres  25842  mbfi1fseqlem4  25846  itg2seq  25870  itg2monolem1  25878  itg2monolem2  25879  itg2monolem3  25880  itg2mono  25881  itg2i1fseq2  25884  itg2gt0  25888  itg2cnlem1  25889  itg2cn  25891  dvne0  26139  lhop2  26143  mdegleb  26190  mdegldg  26192  aalioulem3  26464  logccv  26794  efrlim  27100  basellem3  27213  fsumvma  27343  lgseisenlem4  27508  noseqind  28451  uhgredgn0  29419  upgredgss  29423  umgredgss  29424  edgupgr  29425  upgredg  29428  usgruspgrb  29474  upgrres1  29604  ubthlem1  31163  minvecolem1  31167  htthlem  31210  ofrn  32925  ofrn2  32926  xppreima2  32937  fsumiunle  33114  ccatws1f1olast  33213  mgcf1o  33264  gsumhashmul  33328  xrge0tsmsd  33334  symgcom  33344  cycpmcl  33377  cycpmco2lem1  33387  cycpmco2lem5  33391  cycpmco2  33394  cycpmconjv  33403  cycpmconjslem2  33416  elrgspnsubrunlem2  33509  idomsubr  33573  1arithidom  33772  psrbasfsupp  33846  esplyfv  33905  esplyfval3  33907  ply1degltdimlem  33957  cmpcref  34185  ordtrestNEW  34256  ordtrest2NEW  34258  xrge0mulc1cn  34276  rge0scvg  34284  esumcst  34398  esumpfinvallem  34409  esumpcvgval  34413  esumiun  34429  omssubadd  34635  carsggect  34653  sibfinima  34674  sitgclg  34677  sitgaddlemb  34683  eulerpartgbij  34707  rrvrnss  34782  orvcval4  34796  erdsze2lem2  35595  cvxpconn  35633  cvxsconn  35634  cvmsss2  35665  cvmliftlem8  35683  cvmlift3lem6  35715  mrsubrn  35904  msubrn  35920  mvtss  35944  mclsssvlem  35953  mclsax  35960  mclsind  35961  neibastop2lem  36760  tailfb  36777  knoppcnlem10  36980  lindsdom  38153  poimirlem2  38161  poimirlem11  38170  poimirlem19  38178  poimirlem27  38186  poimirlem30  38189  mblfinlem2  38197  itg2addnclem2  38211  itg2gt0cn  38214  ftc1anclem3  38234  ftc1anclem6  38237  ftc1anclem7  38238  ftc1anc  38240  cnresima  38303  istotbnd3  38310  sstotbnd2  38313  totbndbnd  38328  prdsbnd  38332  cntotbnd  38335  ismtyima  38342  heibor1lem  38348  heibor  38360  rrnequiv  38374  lsatlss  39660  cdleme50rnlem  41208  sticksstones2  42804  aks6d1c6lem5  42834  cmpfiiin  43320  isnacs3  43333  eldioph2lem2  43384  fnwe2lem2  43670  lmhmfgima  43703  cantnfub2  43941  onnoxpg  44047  gneispacern  44756  imo72b2lem2  44785  imo72b2lem1  44787  imo72b2  44790  refsumcn  45642  cncmpmax  45644  elpmrn  45828  climinf  46214  climinf2lem  46312  limsupvaluz2  46344  supcnvlimsup  46346  limsupgtlem  46383  icccncfext  46493  dvsinax  46519  itgsubsticclem  46581  fourierdlem70  46782  fourierdlem82  46794  fourierdlem113  46825  fge0npnf  46973  sge0resrnlem  47009  sge0isum  47033  sge0seq  47052  meadjiunlem  47071  omeiunle  47123  hoicvr  47154  vonvolmbllem  47266  preimaioomnf  47325  smfco  47408  chnsubseqwl  47487  ackvalsucsucval  49353  aacllem  50475