Theorem ssidd 3962

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3907

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

This theorem depends on definitions:  df-bi 210  df-ss 3924

This theorem is referenced by:  pwidg  4578  funfvima2d  7220  suppofss1d  8188  suppofss2d  8189  fpr1  8288  ralxpmap  8882  fissuni  9302  fsuppssov1  9332  fsuppmptif  9347  fsuppco2  9351  fsuppcor  9352  mapfienlem1  9353  mapfienlem2  9354  cantnfp1lem1  9635  cantnfp1lem3  9637  cantnflem1  9646  htalem  9870  ackbij2lem4  10212  cflim2  10235  fin23lem15  10306  wunex2  10711  swrd0  14686  rtrclreclem1  15084  summolem3  15755  isum  15760  fsumser  15771  fsumcl  15774  flo1  15898  prodmolem3  15977  iprod  15982  iprodn0  15984  fprodss  15992  fprodcl  15996  fprodclf  16036  rpnnen2lem11  16270  eulerthlem2  16831  mremre  17646  catsubcat  17886  yon11  18310  yon12  18311  yon2  18312  yonpropd  18314  oppcyon  18315  yonffth  18330  submgmid  18754  submid  18858  mulgnncl  19146  mulgnn0cl  19147  mulgcl  19148  subgid  19185  snsymgefmndeq  19456  symggen  19531  gsumzcl2  19971  gsumzf1o  19973  gsum2dlem1  20031  gsum2dlem2  20032  gsum2d  20033  gsumxp2  20041  dprdfinv  20082  dmdprdsplitlem  20100  dprd2db  20106  dpjidcl  20121  ablfac1eu  20136  ablfaclem2  20149  gsumdixp  20391  subrngid  20625  rnghmsscmap2  20705  rhmsscmap2  20734  fldhmsubc  20857  primefld  20877  lcomfsupp  20992  lss1  21028  rlmbas  21283  rlmplusg  21284  rlm0  21285  rlmmulr  21287  rlmsca  21288  rlmsca2  21289  rlmvsca  21290  rlmtopn  21291  rlmds  21292  rng2idl1cntr  21407  ssdifidl  21445  regsumsupp  21732  frlmsslsp  21906  frlmup1  21908  rnasclassa  22005  mplsubglem  22108  mpllsslem  22109  mplsubrglem  22113  mplcoe1  22148  mplcoe5  22151  mplbas2  22153  evlslem4  22187  psrbagev1  22188  evlslem2  22190  evlsvvvallem  22202  evlsvvvallem2  22203  evlsvvval  22204  mhmcompl  22232  selvcllem4  22249  selvvvval  22253  mhpvscacl  22277  psdmplcl  22285  evls1fpws  22490  evl1maprhm  22500  mamures  22515  cpmadumatpolylem2  23000  neiptopuni  23248  neiptoptop  23249  restopn2  23295  rncmp  23514  cmpfi  23526  conncn  23544  llyidm  23606  nllyidm  23607  toplly  23608  kgentopon  23656  kgencn2  23675  ptcld  23731  qtopuni  23820  supnfcls  24138  utopbas  24353  metustfbas  24675  rrxcph  25512  rrxmval  25525  rrxdstprj1  25529  evthicc2  25580  volcn  25726  dvres3  26033  dvres3a  26034  dvidlem  26035  dvmptresicc  26036  dvcnp2  26040  dvnadd  26049  dvnres  26051  dvaddbr  26058  dvmulbr  26059  dvcmul  26064  dvcmulf  26065  dvcobr  26066  dvcjbr  26069  dvrec  26075  dveflem  26099  dvef  26100  dvlipcn  26114  dvgt0lem2  26123  lhop1lem  26133  ftc1cn  26163  ftc2  26164  itgpowd  26170  deg1mul3le  26235  coeeulem  26342  dgrcolem1  26391  dgrcolem2  26392  plycpn  26411  dvntaylp  26492  pserdv  26550  pige3ALT  26643  cxpcn2  26869  rlimcnp3  27090  lgamgulmlem2  27152  basellem2  27204  pntrsumo1  27687  pntrsumbnd  27688  nosupbnd1lem1  27830  noinfbnd1lem1  27845  cutlt  28083  nbupgr  29603  nbumgrvtx  29605  nbgr2vtx1edg  29609  cusgrexilem2  29701  ifpsnprss  29881  1pthon2ve  30414  suppovss  32938  offinsupp1  32983  xrsmulgzz  33242  gsummpt2co  33281  gsummptrev  33289  gsummptp1  33290  gsumfs2d  33294  gsumpart  33296  gsumhashmul  33300  gsummulsubdishift1  33301  symgcom2  33317  pmtrcnelor  33324  tocycfvres1  33343  tocycfvres2  33344  cycpmconjvlem  33374  elrgspnlem1  33475  elrgspnlem2  33476  elrgspnsubrunlem1  33480  fracf1  33543  idomsubr  33545  fldgenid  33555  lindfpropd  33611  lsmsnpridl  33625  qusrn  33634  elrspunidl  33652  mxidlprm  33670  ssmxidl  33674  selvply1rhmlemb  33826  evlextv  33849  mplvrpmrhm  33854  vieta  33887  srapwov  33896  rlmdim  33917  tngdim  33920  matdim  33922  ply1degltdimlem  33929  fedgmullem1  33936  fldextrspunlsplem  33980  algextdeglem8  34031  constrmon  34051  mdetpmtr1  34130  zarclssn  34180  zart0  34186  zarcmplem  34188  pnfneige0  34258  pwsiga  34437  baselcarsg  34613  boolesineq  34762  efmul2picn  34900  reprfz1  34928  breprexplemc  34936  circlemeth  34944  circlevma  34946  circlemethhgt  34947  hgt750lemb  34960  hgt750lema  34961  hgt750leme  34962  tgoldbachgtde  34964  satfsschain  35727  mrsubff1  35877  mrsub0  35879  mrsubccat  35881  mrsubcn  35882  msubff1  35919  mthmpps  35945  wzel  36185  nmulprop  36553  knoppndvlem6  36968  knoppndv  36985  bj-elpwg  37549  bj-restpw  37594  bj-restb  37596  bj-restuni2  37600  ftc1cnnclem  38202  ftc1cnnc  38203  ftc2nc  38213  areacirclem3  38221  welb  38247  cnresima  38275  rngoidl  38535  1psubclN  40580  cdlemefrs32fva  41036  lcmineqlem9  42666  lcmineqlem12  42669  intlewftc  42690  aks4d1p9  42717  primrootspoweq0  42735  sticksstones11  42785  aks6d1c6lem3  42801  aks6d1c6lem4  42802  aks6d1c6lem5  42806  aks6d1c7lem1  42809  addinvcom  43053  evlselv  43183  rgspnid  43757  oacl2g  43919  omabs2  43921  omcl2  43922  tfsconcatb0  43933  naddgeoa  43983  harval3  44126  cnvtrucl0  44212  brfvrtrcld  44322  clsk3nimkb  44628  k0004ss2  44740  extoimad  44752  mnuprd  44850  dvconstbi  44908  ssinc  45663  ssdec  45664  restopn3  45727  founiiun  45755  choicefi  45775  islptre  46193  fnlimfvre  46246  addccncf2  46448  fsumcncf  46450  cncfperiod  46451  negcncfg  46453  cncfuni  46458  icccncfext  46459  cncficcgt0  46460  fprodcncf  46472  dvcnre  46488  fperdvper  46491  itgsinexplem1  46526  itgcoscmulx  46541  fourierdlem113  46791  smfpimne2  47412  predgclnbgrel  48459  isubgrvtxuhgr  48484  fldhmsubcALTV  48953  elbigolo1  49188  iunlub  49450  iinglb  49451  sepfsepc  49557