Theorem ssidd 3946

Description: Weakening of ssid 3945. (Contributed by BJ, 1-Sep-2022.)

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

Step	Hyp	Ref	Expression
1		ssid 3945	. 2 ⊢ 𝐴 ⊆ 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797

This theorem depends on definitions:  df-bi 207  df-ss 3907

This theorem is referenced by:  funfvima2d  7187  suppofss1d  8154  suppofss2d  8155  fpr1  8253  ralxpmap  8844  fissuni  9267  fsuppssov1  9297  fsuppmptif  9312  fsuppco2  9316  fsuppcor  9317  mapfienlem1  9318  mapfienlem2  9319  cantnfp1lem1  9599  cantnfp1lem3  9601  cantnflem1  9610  htalem  9820  ackbij2lem4  10163  cflim2  10185  fin23lem15  10256  wunex2  10661  swrd0  14621  rtrclreclem1  15019  summolem3  15676  isum  15681  fsumser  15692  fsumcl  15695  flo1  15819  prodmolem3  15898  iprod  15903  iprodn0  15905  fprodss  15913  fprodcl  15917  fprodclf  15957  rpnnen2lem11  16191  eulerthlem2  16752  mremre  17566  catsubcat  17806  yon11  18230  yon12  18231  yon2  18232  yonpropd  18234  oppcyon  18235  yonffth  18250  submgmid  18674  submid  18778  mulgnncl  19065  mulgnn0cl  19066  mulgcl  19067  subgid  19104  snsymgefmndeq  19370  symggen  19445  gsumzcl2  19885  gsumzf1o  19887  gsum2dlem1  19945  gsum2dlem2  19946  gsum2d  19947  gsumxp2  19955  dprdfinv  19996  dmdprdsplitlem  20014  dprd2db  20020  dpjidcl  20035  ablfac1eu  20050  ablfaclem2  20063  gsumdixp  20298  subrngid  20526  rnghmsscmap2  20606  rhmsscmap2  20635  fldhmsubc  20762  primefld  20782  lcomfsupp  20897  lss1  20933  rlmbas  21188  rlmplusg  21189  rlm0  21190  rlmmulr  21192  rlmsca  21193  rlmsca2  21194  rlmvsca  21195  rlmtopn  21196  rlmds  21197  rng2idl1cntr  21303  regsumsupp  21602  frlmsslsp  21776  frlmup1  21778  rnasclassa  21875  mplsubglem  21977  mpllsslem  21978  mplsubrglem  21982  mplcoe1  22015  mplcoe5  22018  mplbas2  22020  evlslem4  22054  psrbagev1  22055  evlslem2  22057  evlsvvvallem  22069  evlsvvvallem2  22070  evlsvvval  22071  mhpvscacl  22120  psdmplcl  22128  evls1fpws  22334  evl1maprhm  22344  mhmcompl  22345  mamures  22362  cpmadumatpolylem2  22847  neiptopuni  23095  neiptoptop  23096  restopn2  23142  rncmp  23361  cmpfi  23373  conncn  23391  llyidm  23453  nllyidm  23454  toplly  23455  kgentopon  23503  kgencn2  23522  ptcld  23578  qtopuni  23667  supnfcls  23985  utopbas  24200  metustfbas  24522  rrxcph  25359  rrxmval  25372  rrxdstprj1  25376  evthicc2  25427  volcn  25573  dvres3  25880  dvres3a  25881  dvidlem  25882  dvmptresicc  25883  dvcnp2  25887  dvnadd  25896  dvnres  25898  dvaddbr  25905  dvmulbr  25906  dvcmul  25911  dvcmulf  25912  dvcobr  25913  dvcjbr  25916  dvrec  25922  dveflem  25946  dvef  25947  dvlipcn  25961  dvgt0lem2  25970  lhop1lem  25980  ftc1cn  26010  ftc2  26011  itgpowd  26017  deg1mul3le  26082  coeeulem  26189  dgrcolem1  26238  dgrcolem2  26239  plycpn  26255  dvntaylp  26336  pserdv  26394  pige3ALT  26484  cxpcn2  26710  rlimcnp3  26931  lgamgulmlem2  26993  basellem2  27045  pntrsumo1  27528  pntrsumbnd  27529  nosupbnd1lem1  27672  noinfbnd1lem1  27687  cutlt  27924  nbupgr  29413  nbumgrvtx  29415  nbgr2vtx1edg  29419  cusgrexilem2  29511  ifpsnprss  29691  1pthon2ve  30224  suppovss  32754  offinsupp1  32799  xrsmulgzz  33069  gsummpt2co  33109  gsummptrev  33117  gsummptp1  33118  gsumfs2d  33122  gsumpart  33124  gsumhashmul  33128  gsummulsubdishift1  33129  symgcom2  33145  pmtrcnelor  33152  tocycfvres1  33171  tocycfvres2  33172  cycpmconjvlem  33202  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnsubrunlem1  33308  fracf1  33368  idomsubr  33370  fldgenid  33380  lindfpropd  33442  lsmsnpridl  33458  qusrn  33469  elrspunidl  33488  ssdifidl  33517  mxidlprm  33530  ssmxidl  33534  evlextv  33686  mplvrpmrhm  33691  vieta  33724  srapwov  33733  rlmdim  33754  tngdim  33757  matdim  33759  ply1degltdimlem  33766  fedgmullem1  33773  fldextrspunlsplem  33817  algextdeglem8  33868  constrmon  33888  mdetpmtr1  33967  zarclssn  34017  zart0  34023  zarcmplem  34025  pnfneige0  34095  pwsiga  34274  baselcarsg  34450  boolesineq  34599  efmul2picn  34740  reprfz1  34768  breprexplemc  34776  circlemeth  34784  circlevma  34786  circlemethhgt  34787  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  tgoldbachgtde  34804  satfsschain  35546  mrsubff1  35696  mrsub0  35698  mrsubccat  35700  mrsubcn  35701  msubff1  35738  mthmpps  35764  wzel  36004  knoppndvlem6  36777  knoppndv  36794  bj-elpwg  37359  bj-restpw  37404  bj-restb  37406  bj-restuni2  37410  ftc1cnnclem  38012  ftc1cnnc  38013  ftc2nc  38023  areacirclem3  38031  welb  38057  cnresima  38085  rngoidl  38345  1psubclN  40390  cdlemefrs32fva  40846  lcmineqlem9  42476  lcmineqlem12  42479  intlewftc  42500  aks4d1p9  42527  primrootspoweq0  42545  sticksstones11  42595  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6lem5  42616  aks6d1c7lem1  42619  addinvcom  42864  selvcllem4  43014  selvvvval  43018  evlselv  43020  rgspnid  43596  oacl2g  43758  omabs2  43760  omcl2  43761  tfsconcatb0  43772  naddgeoa  43822  harval3  43965  cnvtrucl0  44051  brfvrtrcld  44161  clsk3nimkb  44467  k0004ss2  44579  extoimad  44591  mnuprd  44703  dvconstbi  44761  ssinc  45517  ssdec  45518  restopn3  45581  founiiun  45609  choicefi  45629  islptre  46049  fnlimfvre  46102  addccncf2  46304  fsumcncf  46306  cncfperiod  46307  negcncfg  46309  cncfuni  46314  icccncfext  46315  cncficcgt0  46316  fprodcncf  46328  dvcnre  46344  fperdvper  46347  itgsinexplem1  46382  itgcoscmulx  46397  smfpimne2  47268  predgclnbgrel  48309  isubgrvtxuhgr  48334  fldhmsubcALTV  48803  elbigolo1  49027  iunlub  49290  iinglb  49291  sepfsepc  49397