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 3904

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

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

This theorem is referenced by:  pwidg  4581  funfvima2d  7230  suppofss1d  8199  suppofss2d  8200  fpr1  8299  ralxpmap  8893  fissuni  9313  fsuppssov1  9343  fsuppmptif  9358  fsuppco2  9362  fsuppcor  9363  mapfienlem1  9364  mapfienlem2  9365  cantnfp1lem1  9646  cantnfp1lem3  9648  cantnflem1  9657  htalem  9881  ackbij2lem4  10223  cflim2  10246  fin23lem15  10317  wunex2  10722  swrd0  14696  rtrclreclem1  15094  summolem3  15765  isum  15770  fsumser  15781  fsumcl  15784  flo1  15908  prodmolem3  15987  iprod  15992  iprodn0  15994  fprodss  16002  fprodcl  16006  fprodclf  16046  rpnnen2lem11  16279  eulerthlem2  16840  mremre  17655  catsubcat  17895  yon11  18319  yon12  18320  yon2  18321  yonpropd  18323  oppcyon  18324  yonffth  18339  submgmid  18763  submid  18867  mulgnncl  19154  mulgnn0cl  19155  mulgcl  19156  subgid  19193  snsymgefmndeq  19464  symggen  19539  gsumzcl2  19979  gsumzf1o  19981  gsum2dlem1  20039  gsum2dlem2  20040  gsum2d  20041  gsumxp2  20049  dprdfinv  20090  dmdprdsplitlem  20108  dprd2db  20114  dpjidcl  20129  ablfac1eu  20144  ablfaclem2  20157  gsumdixp  20399  subrngid  20633  rnghmsscmap2  20713  rhmsscmap2  20742  fldhmsubc  20867  primefld  20887  lcomfsupp  21002  lss1  21038  rlmbas  21293  rlmplusg  21294  rlm0  21295  rlmmulr  21297  rlmsca  21298  rlmsca2  21299  rlmvsca  21300  rlmtopn  21301  rlmds  21302  rng2idl1cntr  21424  ssdifidl  21464  regsumsupp  21751  frlmsslsp  21925  frlmup1  21927  rnasclassa  22024  mplsubglem  22127  mpllsslem  22128  mplsubrglem  22132  mplcoe1  22167  mplcoe5  22170  mplbas2  22172  evlslem4  22206  psrbagev1  22207  evlslem2  22209  evlsvvvallem  22221  evlsvvvallem2  22222  evlsvvval  22223  mhmcompl  22251  selvcllem4  22268  selvvvval  22272  mhpvscacl  22296  psdmplcl  22304  evls1fpws  22508  evl1maprhm  22518  mamures  22533  cpmadumatpolylem2  23018  neiptopuni  23266  neiptoptop  23267  restopn2  23313  rncmp  23532  cmpfi  23544  conncn  23562  llyidm  23624  nllyidm  23625  toplly  23626  kgentopon  23674  kgencn2  23693  ptcld  23749  qtopuni  23838  supnfcls  24156  utopbas  24371  metustfbas  24693  rrxcph  25530  rrxmval  25543  rrxdstprj1  25547  evthicc2  25598  volcn  25744  dvres3  26051  dvres3a  26052  dvidlem  26053  dvmptresicc  26054  dvcnp2  26058  dvnadd  26067  dvnres  26069  dvaddbr  26076  dvmulbr  26077  dvcmul  26082  dvcmulf  26083  dvcobr  26084  dvcjbr  26087  dvrec  26093  dveflem  26117  dvef  26118  dvlipcn  26132  dvgt0lem2  26141  lhop1lem  26151  ftc1cn  26181  ftc2  26182  itgpowd  26188  deg1mul3le  26253  coeeulem  26360  dgrcolem1  26409  dgrcolem2  26410  plycpn  26429  dvntaylp  26510  pserdv  26568  pige3ALT  26661  cxpcn2  26887  rlimcnp3  27108  lgamgulmlem2  27170  basellem2  27222  pntrsumo1  27705  pntrsumbnd  27706  nosupbnd1lem1  27848  noinfbnd1lem1  27863  cutlt  28101  nbupgr  29660  nbumgrvtx  29662  nbgr2vtx1edg  29666  cusgrexilem2  29758  ifpsnprss  29938  1pthon2ve  30471  suppovss  32992  offinsupp1  33037  xrsmulgzz  33295  gsummpt2co  33334  gsummptrev  33342  gsummptp1  33343  gsumfs2d  33347  gsumpart  33349  gsumhashmul  33353  gsummulsubdishift1  33354  symgcom2  33370  pmtrcnelor  33377  tocycfvres1  33396  tocycfvres2  33397  cycpmconjvlem  33427  elrgspnlem1  33528  elrgspnlem2  33529  elrgspnsubrunlem1  33533  fracf1  33594  idomsubr  33596  fldgenid  33606  lindfpropd  33661  lsmsnpridl  33675  qusrn  33684  elrspunidl  33702  mxidlprm  33719  ssmxidl  33723  selvply1rhmlemb  33875  evlextv  33898  mplvrpmrhm  33903  vieta  33936  srapwov  33945  rlmdim  33966  tngdim  33969  matdim  33971  ply1degltdimlem  33978  fedgmullem1  33985  fldextrspunlsplem  34029  algextdeglem8  34080  constrmon  34100  mdetpmtr1  34179  zarclssn  34229  zart0  34235  zarcmplem  34237  pnfneige0  34307  pwsiga  34486  baselcarsg  34662  boolesineq  34811  efmul2picn  34949  reprfz1  34977  breprexplemc  34985  circlemeth  34993  circlevma  34995  circlemethhgt  34996  hgt750lemb  35009  hgt750lema  35010  hgt750leme  35011  tgoldbachgtde  35013  satfsschain  35822  mrsubff1  35972  mrsub0  35974  mrsubccat  35976  mrsubcn  35977  msubff1  36014  mthmpps  36040  wzel  36280  nmulprop  36648  knoppndvlem6  37072  knoppndv  37089  bj-elpwg  37654  bj-restpw  37700  bj-restb  37702  bj-restuni2  37706  ftc1cnnclem  38308  ftc1cnnc  38309  ftc2nc  38319  areacirclem3  38327  welb  38353  cnresima  38381  rngoidl  38641  1psubclN  40686  cdlemefrs32fva  41142  lcmineqlem9  42772  lcmineqlem12  42775  intlewftc  42796  aks4d1p9  42823  primrootspoweq0  42841  sticksstones11  42891  aks6d1c6lem3  42907  aks6d1c6lem4  42908  aks6d1c6lem5  42912  aks6d1c7lem1  42915  addinvcom  43161  evlselv  43291  rgspnid  43865  oacl2g  44027  omabs2  44029  omcl2  44030  tfsconcatb0  44041  naddgeoa  44091  harval3  44234  cnvtrucl0  44320  brfvrtrcld  44430  clsk3nimkb  44736  k0004ss2  44848  extoimad  44860  mnuprd  44956  dvconstbi  45014  ssinc  45775  ssdec  45776  restopn3  45839  founiiun  45867  choicefi  45887  islptre  46305  fnlimfvre  46358  addccncf2  46560  fsumcncf  46562  cncfperiod  46563  negcncfg  46565  cncfuni  46570  icccncfext  46571  cncficcgt0  46572  fprodcncf  46584  dvcnre  46600  fperdvper  46603  itgsinexplem1  46638  itgcoscmulx  46653  fourierdlem113  46903  smfpimne2  47524  predgclnbgrel  48571  isubgrvtxuhgr  48596  fldhmsubcALTV  49065  elbigolo1  49304  iunlub  49566  iinglb  49567  sepfsepc  49673