Theorem frnd 6696

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

Syntax hints:   → wi 4   ⊆ wss 3914  ran crn 5639  ⟶wf 6507

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 207  df-an 396  df-f 6515

This theorem is referenced by:  f1un  6820  fliftrel  7283  f1iun  7922  f1dmex  7935  fo2ndf  8100  onoviun  8312  onnseq  8313  smores2  8323  domdifsn  9024  omxpenlem  9042  fodomr  9092  domss2  9100  f1domfi  9145  sucdom2  9167  f1finf1o  9216  f1finf1oOLD  9217  infn0  9251  f1fi  9263  fodomfir  9279  unirnffid  9298  intrnfi  9367  dffi3  9382  ordtypelem8  9478  ordtypelem9  9479  ordtypelem10  9480  hartogslem1  9495  brwdom2  9526  unxpwdom2  9541  ixpiunwdom  9543  infdifsn  9610  cantnf  9646  ac10ct  9987  numacn  10002  infpwfien  10015  fictb  10197  isf34lem5  10331  isf34lem7  10332  isf34lem6  10333  enfin1ai  10337  canthp1lem2  10606  gch3  10629  wuncval2  10700  peano5nni  12189  hashimarn  14405  hashf1lem1  14420  hashf1lem2  14421  ccatrn  14554  swrdrn  14617  pfxrn  14650  cshwrn  14767  limsupgle  15443  limsupgre  15447  isercolllem2  15632  isercoll  15634  isercoll2  15635  climsup  15636  ruclem11  16208  4sqlem11  16926  vdwapf  16943  vdwlem11  16962  0ram  16991  funcres2b  17859  funcres2c  17865  setcepi  18050  yoniso  18246  isacs4lem  18503  mgmhmima  18642  mhmima  18752  gsumwspan  18773  frmdss2  18790  cycsubm  19134  cycsubgcl  19138  cycsubgss  19139  ghmrn  19161  conjnmz  19184  ghmqusnsg  19214  ghmquskerlem3  19218  cntzmhm  19273  f1omvdconj  19376  odf1o2  19503  pgpssslw  19544  sylow2blem1  19550  lsmssv  19573  smndlsmidm  19586  pj1ghm2  19634  efgsp1  19667  efgrelexlemb  19680  cntzcmnf  19775  cyggenod  19814  gsumval3eu  19834  gsumval3lem2  19836  gsumval3  19837  gsumzsubmcl  19848  gsumzaddlem  19851  gsumzadd  19852  gsumzsplit  19857  gsumconst  19864  gsumzoppg  19874  gsumpt  19892  dmdprdd  19931  dprdfcntz  19947  dprdfeq0  19954  dprdlub  19958  dprdres  19960  dprdss  19961  dprdz  19962  subgdprd  19967  dprd2dlem1  19973  dprd2da  19974  dmdprdsplit2lem  19977  dpjghm2  19996  ablfac1b  20002  lmhmlsp  20956  pj1lmhm2  21008  pjfo  21624  frlmsplit2  21682  frlmsslsp  21705  frlmlbs  21706  frlmup3  21709  frlmup4  21710  lindff1  21729  lindfrn  21730  f1lindf  21731  indlcim  21749  aspval2  21807  mplcoe5lem  21946  mplbas2  21949  mplind  21977  evlslem1  21989  evlseu  21990  gsumply1subr  22118  m2cpmf1  22630  m2cpmghm  22631  iinopn  22789  pptbas  22895  tgrest  23046  resttopon  23048  rest0  23056  restfpw  23066  ordtbaslem  23075  ordtuni  23077  ordtbas2  23078  ordtrest  23089  ordtrest2  23091  cnclsi  23159  cnrest2r  23174  cnprest2  23177  lmss  23185  cncmp  23279  rncmp  23283  discmp  23285  connima  23312  conncn  23313  2ndcdisj  23343  2ndcomap  23345  dis2ndc  23347  lly1stc  23383  comppfsc  23419  kgencmp  23432  1stckgenlem  23440  kgencn3  23445  ptbasfi  23468  txbasval  23493  upxp  23510  uptx  23512  txtube  23527  txcmplem1  23528  txcmplem2  23529  tx1stc  23537  xkoptsub  23541  xkoco2cn  23545  xkococnlem  23546  hmeores  23658  fbasrn  23771  trfilss  23776  trfg  23778  uzrest  23784  rnelfmlem  23839  fclscmpi  23916  alexsublem  23931  ptcmplem1  23939  ptcmplem3  23941  cnextcn  23954  tmdgsum2  23983  subgtgp  23992  subgntr  23994  opnsubg  23995  clsnsg  23997  tgpconncomp  24000  tsmsfbas  24015  prdsdsf  24255  prdsxmetlem  24256  prdsmet  24258  imasdsf1olem  24261  unirnblps  24307  unirnbl  24308  prdsbl  24379  met1stc  24409  met2ndci  24410  prdsxmslem2  24417  xrge0gsumle  24722  xrge0tsms  24723  metdcn2  24728  metdsf  24737  metdsge  24738  cnmptre  24821  bndth  24857  evth  24858  evth2  24859  lebnumlem2  24861  lebnumlem3  24862  reparphti  24896  reparphtiOLD  24897  bcthlem5  25228  minveclem1  25324  minveclem3b  25328  evthicc2  25361  ovolmge0  25378  ovollb  25380  ovolgelb  25381  ovollb2lem  25389  ovollb2  25390  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliun  25406  ovoliun2  25407  ovolscalem1  25414  ovolicc1  25417  ovolicc2lem4  25421  ovolicc2  25423  voliunlem2  25452  voliunlem3  25453  ioombl1lem2  25460  ioombl1lem4  25462  uniioovol  25480  uniiccvol  25481  uniioombllem1  25482  uniioombllem2  25484  uniioombllem3  25486  uniioombllem6  25489  uniioombl  25490  volsup2  25506  vitalilem2  25510  vitalilem4  25512  vitalilem5  25513  mbfsup  25565  mbfinf  25566  mbflimsup  25567  i1fima  25579  i1fima2  25580  itg1cl  25586  itg1ge0  25587  i1fmullem  25595  i1fadd  25596  i1fmul  25597  itg1addlem4  25600  itg1addlem5  25601  i1fmulc  25604  itg1mulc  25605  i1fres  25606  itg10a  25611  itg1ge0a  25612  itg1climres  25615  mbfi1fseqlem4  25619  itg2seq  25643  itg2monolem1  25651  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  itg2i1fseq2  25657  itg2gt0  25661  itg2cnlem1  25662  itg2cn  25664  dvne0  25916  lhop2  25920  mdegleb  25969  mdegldg  25971  aalioulem3  26242  logccv  26572  efrlim  26879  efrlimOLD  26880  basellem3  26993  fsumvma  27124  lgseisenlem4  27289  noseqind  28186  uhgredgn0  29055  upgredgss  29059  umgredgss  29060  edgupgr  29061  upgredg  29064  usgruspgrb  29110  upgrres1  29240  ubthlem1  30799  minvecolem1  30803  htthlem  30846  ofrn  32563  ofrn2  32564  xppreima2  32575  fsumiunle  32754  ccatws1f1olast  32874  mgcf1o  32929  chnso  32940  gsumhashmul  33001  xrge0tsmsd  33002  symgcom  33040  cycpmcl  33073  cycpmco2lem1  33083  cycpmco2lem5  33087  cycpmco2  33090  cycpmconjv  33099  cycpmconjslem2  33112  elrgspnsubrunlem2  33199  idomsubr  33259  1arithidom  33508  ply1degltdimlem  33618  cmpcref  33840  ordtrestNEW  33911  ordtrest2NEW  33913  xrge0mulc1cn  33931  rge0scvg  33939  esumcst  34053  esumpfinvallem  34064  esumpcvgval  34068  esumiun  34084  omssubadd  34291  carsggect  34309  sibfinima  34330  sitgclg  34333  sitgaddlemb  34339  eulerpartgbij  34363  rrvrnss  34438  orvcval4  34452  erdsze2lem2  35191  cvxpconn  35229  cvxsconn  35230  cvmsss2  35261  cvmliftlem8  35279  cvmlift3lem6  35311  mrsubrn  35500  msubrn  35516  mvtss  35540  mclsssvlem  35549  mclsax  35556  mclsind  35557  neibastop2lem  36348  tailfb  36365  knoppcnlem10  36490  lindsdom  37608  poimirlem2  37616  poimirlem11  37625  poimirlem19  37633  poimirlem27  37641  poimirlem30  37644  mblfinlem2  37652  itg2addnclem2  37666  itg2gt0cn  37669  ftc1anclem3  37689  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anc  37695  cnresima  37758  istotbnd3  37765  sstotbnd2  37768  totbndbnd  37783  prdsbnd  37787  cntotbnd  37790  ismtyima  37797  heibor1lem  37803  heibor  37815  rrnequiv  37829  lsatlss  38989  cdleme50rnlem  40538  sticksstones2  42135  aks6d1c6lem5  42165  cmpfiiin  42685  isnacs3  42698  eldioph2lem2  42749  fnwe2lem2  43040  lmhmfgima  43073  cantnfub2  43311  onnog  43418  gneispacern  44127  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  refsumcn  45024  cncmpmax  45026  elpmrn  45214  climinf  45604  climinf2lem  45704  limsupvaluz2  45736  supcnvlimsup  45738  limsupgtlem  45775  icccncfext  45885  dvsinax  45911  itgsubsticclem  45973  fourierdlem70  46174  fourierdlem82  46186  fge0npnf  46365  sge0resrnlem  46401  sge0isum  46425  sge0seq  46444  meadjiunlem  46463  omeiunle  46515  hoicvr  46546  vonvolmbllem  46658  preimaioomnf  46717  smfco  46800  ackvalsucsucval  48677  aacllem  49790