Theorem ssidd 3959

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3903

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 3920

This theorem is referenced by:  funfvima2d  7188  suppofss1d  8156  suppofss2d  8157  fpr1  8255  ralxpmap  8846  fissuni  9269  fsuppssov1  9299  fsuppmptif  9314  fsuppco2  9318  fsuppcor  9319  mapfienlem1  9320  mapfienlem2  9321  cantnfp1lem1  9599  cantnfp1lem3  9601  cantnflem1  9610  htalem  9820  ackbij2lem4  10163  cflim2  10185  fin23lem15  10256  wunex2  10661  swrd0  14594  rtrclreclem1  14992  summolem3  15649  isum  15654  fsumser  15665  fsumcl  15668  flo1  15789  prodmolem3  15868  iprod  15873  iprodn0  15875  fprodss  15883  fprodcl  15887  fprodclf  15927  rpnnen2lem11  16161  eulerthlem2  16721  mremre  17535  catsubcat  17775  yon11  18199  yon12  18200  yon2  18201  yonpropd  18203  oppcyon  18204  yonffth  18219  submgmid  18643  submid  18747  mulgnncl  19031  mulgnn0cl  19032  mulgcl  19033  subgid  19070  snsymgefmndeq  19336  symggen  19411  gsumzcl2  19851  gsumzf1o  19853  gsum2dlem1  19911  gsum2dlem2  19912  gsum2d  19913  gsumxp2  19921  dprdfinv  19962  dmdprdsplitlem  19980  dprd2db  19986  dpjidcl  20001  ablfac1eu  20016  ablfaclem2  20029  gsumdixp  20266  subrngid  20494  rnghmsscmap2  20574  rhmsscmap2  20603  fldhmsubc  20730  primefld  20750  lcomfsupp  20865  lss1  20901  rlmbas  21157  rlmplusg  21158  rlm0  21159  rlmmulr  21161  rlmsca  21162  rlmsca2  21163  rlmvsca  21164  rlmtopn  21165  rlmds  21166  rng2idl1cntr  21272  regsumsupp  21589  frlmsslsp  21763  frlmup1  21765  rnasclassa  21863  mplsubglem  21966  mpllsslem  21967  mplsubrglem  21971  mplcoe1  22004  mplcoe5  22007  mplbas2  22009  evlslem4  22043  psrbagev1  22044  evlslem2  22046  evlsvvvallem  22058  evlsvvvallem2  22059  evlsvvval  22060  mhpvscacl  22109  psdmplcl  22117  evls1fpws  22325  evl1maprhm  22335  mhmcompl  22336  mamures  22353  cpmadumatpolylem2  22838  neiptopuni  23086  neiptoptop  23087  restopn2  23133  rncmp  23352  cmpfi  23364  conncn  23382  llyidm  23444  nllyidm  23445  toplly  23446  kgentopon  23494  kgencn2  23513  ptcld  23569  qtopuni  23658  supnfcls  23976  utopbas  24191  metustfbas  24513  rrxcph  25360  rrxmval  25373  rrxdstprj1  25377  evthicc2  25429  volcn  25575  dvres3  25882  dvres3a  25883  dvidlem  25884  dvmptresicc  25885  dvcnp2  25889  dvnadd  25899  dvnres  25901  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcmul  25915  dvcmulf  25916  dvcobr  25917  dvcobrOLD  25918  dvcjbr  25921  dvrec  25927  dveflem  25951  dvef  25952  dvlipcn  25967  dvgt0lem2  25976  lhop1lem  25986  ftc1cn  26018  ftc2  26019  itgpowd  26025  deg1mul3le  26090  coeeulem  26197  dgrcolem1  26247  dgrcolem2  26248  plycpn  26265  dvntaylp  26347  pserdv  26407  pige3ALT  26497  cxpcn2  26724  rlimcnp3  26945  lgamgulmlem2  27008  basellem2  27060  pntrsumo1  27544  pntrsumbnd  27545  nosupbnd1lem1  27688  noinfbnd1lem1  27703  cutlt  27940  nbupgr  29429  nbumgrvtx  29431  nbgr2vtx1edg  29435  cusgrexilem2  29527  ifpsnprss  29708  1pthon2ve  30241  suppovss  32770  offinsupp1  32815  xrsmulgzz  33101  gsummpt2co  33141  gsummptrev  33149  gsummptp1  33150  gsumfs2d  33154  gsumpart  33156  gsumhashmul  33160  gsummulsubdishift1  33161  symgcom2  33177  pmtrcnelor  33184  tocycfvres1  33203  tocycfvres2  33204  cycpmconjvlem  33234  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnsubrunlem1  33340  fracf1  33400  idomsubr  33402  fldgenid  33412  lindfpropd  33474  lsmsnpridl  33490  qusrn  33501  elrspunidl  33520  ssdifidl  33549  mxidlprm  33562  ssmxidl  33566  evlextv  33718  mplvrpmrhm  33723  vieta  33756  srapwov  33765  rlmdim  33786  rgmoddimOLD  33787  tngdim  33790  matdim  33792  ply1degltdimlem  33799  fedgmullem1  33806  fldextrspunlsplem  33850  algextdeglem8  33901  constrmon  33921  mdetpmtr1  34000  zarclssn  34050  zart0  34056  zarcmplem  34058  pnfneige0  34128  pwsiga  34307  baselcarsg  34483  boolesineq  34632  efmul2picn  34773  reprfz1  34801  breprexplemc  34809  circlemeth  34817  circlevma  34819  circlemethhgt  34820  hgt750lemb  34833  hgt750lema  34834  hgt750leme  34835  tgoldbachgtde  34837  satfsschain  35577  mrsubff1  35727  mrsub0  35729  mrsubccat  35731  mrsubcn  35732  msubff1  35769  mthmpps  35795  wzel  36035  knoppndvlem6  36736  knoppndv  36753  bj-elpwg  37291  bj-restpw  37336  bj-restb  37338  bj-restuni2  37342  ftc1cnnclem  37931  ftc1cnnc  37932  ftc2nc  37942  areacirclem3  37950  welb  37976  cnresima  38004  rngoidl  38264  1psubclN  40309  cdlemefrs32fva  40765  lcmineqlem9  42396  lcmineqlem12  42399  intlewftc  42420  aks4d1p9  42447  primrootspoweq0  42465  sticksstones11  42515  aks6d1c6lem3  42531  aks6d1c6lem4  42532  aks6d1c6lem5  42536  aks6d1c7lem1  42539  addinvcom  42791  selvcllem4  42928  selvvvval  42932  evlselv  42934  rgspnid  43514  oacl2g  43676  omabs2  43678  omcl2  43679  tfsconcatb0  43690  naddgeoa  43740  harval3  43883  cnvtrucl0  43969  brfvrtrcld  44079  clsk3nimkb  44385  k0004ss2  44497  extoimad  44509  mnuprd  44621  dvconstbi  44679  ssinc  45435  ssdec  45436  restopn3  45499  founiiun  45527  choicefi  45547  islptre  45968  fnlimfvre  46021  addccncf2  46223  fsumcncf  46225  cncfperiod  46226  negcncfg  46228  cncfuni  46233  icccncfext  46234  cncficcgt0  46235  fprodcncf  46247  dvcnre  46263  fperdvper  46266  itgsinexplem1  46301  itgcoscmulx  46316  smfpimne2  47187  predgclnbgrel  48188  isubgrvtxuhgr  48213  fldhmsubcALTV  48682  elbigolo1  48906  iunlub  49169  iinglb  49170  sepfsepc  49276