Theorem ssidd 4018

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3962

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

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

This theorem is referenced by:  funfvima2d  7251  suppofss1d  8227  suppofss2d  8228  fpr1  8326  ralxpmap  8934  fissuni  9394  fsuppssov1  9421  fsuppmptif  9436  fsuppco2  9440  fsuppcor  9441  mapfienlem1  9442  mapfienlem2  9443  cantnfp1lem1  9715  cantnfp1lem3  9717  cantnflem1  9726  htalem  9933  ackbij2lem4  10278  cflim2  10300  fin23lem15  10371  wunex2  10775  swrd0  14692  rtrclreclem1  15092  summolem3  15746  isum  15751  fsumser  15762  fsumcl  15765  flo1  15886  prodmolem3  15965  iprod  15970  iprodn0  15972  fprodss  15980  fprodcl  15984  fprodclf  16024  rpnnen2lem11  16256  eulerthlem2  16815  mremre  17648  catsubcat  17889  yon11  18320  yon12  18321  yon2  18322  yonpropd  18324  oppcyon  18325  yonffth  18340  submgmid  18731  submid  18835  mulgnncl  19119  mulgnn0cl  19120  mulgcl  19121  subgid  19158  snsymgefmndeq  19426  symggen  19502  gsumzcl2  19942  gsumzf1o  19944  gsum2dlem1  20002  gsum2dlem2  20003  gsum2d  20004  gsumxp2  20012  dprdfinv  20053  dmdprdsplitlem  20071  dprd2db  20077  dpjidcl  20092  ablfac1eu  20107  ablfaclem2  20120  gsumdixp  20332  subrngid  20565  rnghmsscmap2  20645  rhmsscmap2  20674  fldhmsubc  20802  primefld  20822  lcomfsupp  20916  lss1  20953  rlmbas  21217  rlmplusg  21218  rlm0  21219  rlmmulr  21221  rlmsca  21222  rlmsca2  21223  rlmvsca  21224  rlmtopn  21225  rlmds  21226  rng2idl1cntr  21332  regsumsupp  21657  frlmsslsp  21833  frlmup1  21835  rnasclassa  21932  mplsubglem  22036  mpllsslem  22037  mplsubrglem  22041  mplcoe1  22072  mplcoe5  22075  mplbas2  22077  evlslem4  22117  psrbagev1  22118  evlslem2  22120  mhpvscacl  22175  psdmplcl  22183  evls1fpws  22388  evl1maprhm  22398  mhmcompl  22399  mamures  22416  cpmadumatpolylem2  22903  neiptopuni  23153  neiptoptop  23154  restopn2  23200  rncmp  23419  cmpfi  23431  conncn  23449  llyidm  23511  nllyidm  23512  toplly  23513  kgentopon  23561  kgencn2  23580  ptcld  23636  qtopuni  23725  supnfcls  24043  utopbas  24259  metustfbas  24585  rrxcph  25439  rrxmval  25452  rrxdstprj1  25456  evthicc2  25508  volcn  25654  dvres3  25962  dvres3a  25963  dvidlem  25964  dvmptresicc  25965  dvcnp2  25969  dvnadd  25979  dvnres  25981  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcmul  25995  dvcmulf  25996  dvcobr  25997  dvcobrOLD  25998  dvcjbr  26001  dvrec  26007  dveflem  26031  dvef  26032  dvlipcn  26047  dvgt0lem2  26056  lhop1lem  26066  ftc1cn  26098  ftc2  26099  itgpowd  26105  deg1mul3le  26170  coeeulem  26277  dgrcolem1  26327  dgrcolem2  26328  plycpn  26345  dvntaylp  26427  pserdv  26487  pige3ALT  26576  cxpcn2  26803  rlimcnp3  27024  lgamgulmlem2  27087  basellem2  27139  pntrsumo1  27623  pntrsumbnd  27624  nosupbnd1lem1  27767  noinfbnd1lem1  27782  cutlt  27980  nbupgr  29375  nbumgrvtx  29377  nbgr2vtx1edg  29381  cusgrexilem2  29473  ifpsnprss  29655  1pthon2ve  30182  suppovss  32695  offinsupp1  32744  xrsmulgzz  32993  gsummpt2co  33033  gsumfs2d  33040  gsumpart  33042  gsumhashmul  33046  symgcom2  33086  pmtrcnelor  33093  tocycfvres1  33112  tocycfvres2  33113  cycpmconjvlem  33143  elrgspnlem1  33231  elrgspnlem2  33232  fracf1  33288  idomsubr  33290  fldgenid  33300  lindfpropd  33389  lsmsnpridl  33405  qusrn  33416  elrspunidl  33435  ssdifidl  33464  mxidlprm  33477  ssmxidl  33481  rlmdim  33636  rgmoddimOLD  33637  tngdim  33640  matdim  33642  ply1degltdimlem  33649  fedgmullem1  33656  algextdeglem8  33729  constrmon  33748  mdetpmtr1  33783  zarclssn  33833  zart0  33839  zarcmplem  33841  pnfneige0  33911  pwsiga  34110  baselcarsg  34287  efmul2picn  34589  reprfz1  34617  breprexplemc  34625  circlemeth  34633  circlevma  34635  circlemethhgt  34636  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  tgoldbachgtde  34653  satfsschain  35348  mrsubff1  35498  mrsub0  35500  mrsubccat  35502  mrsubcn  35503  msubff1  35540  mthmpps  35566  wzel  35805  knoppndvlem6  36499  knoppndv  36516  bj-elpwg  37034  bj-restpw  37074  bj-restb  37076  bj-restuni2  37080  ftc1cnnclem  37677  ftc1cnnc  37678  ftc2nc  37688  areacirclem3  37696  welb  37722  cnresima  37750  rngoidl  38010  1psubclN  39926  cdlemefrs32fva  40382  lcmineqlem9  42018  lcmineqlem12  42021  intlewftc  42042  aks4d1p9  42069  primrootspoweq0  42087  sticksstones11  42137  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6lem5  42158  aks6d1c7lem1  42161  addinvcom  42437  evlsvvvallem  42547  evlsvvvallem2  42548  evlsvvval  42549  selvcllem4  42567  selvvvval  42571  evlselv  42573  rgspnid  43156  oacl2g  43319  omabs2  43321  omcl2  43322  tfsconcatb0  43333  naddgeoa  43383  harval3  43527  cnvtrucl0  43613  brfvrtrcld  43723  clsk3nimkb  44029  k0004ss2  44141  extoimad  44153  mnuprd  44271  dvconstbi  44329  ssinc  45026  ssdec  45027  restopn3  45093  founiiun  45121  choicefi  45142  islptre  45574  fnlimfvre  45629  addccncf2  45831  fsumcncf  45833  cncfperiod  45834  negcncfg  45836  cncfuni  45841  icccncfext  45842  cncficcgt0  45843  fprodcncf  45855  dvcnre  45871  fperdvper  45874  itgsinexplem1  45909  itgcoscmulx  45924  smfpimne2  46795  predgclnbgrel  47762  isubgrvtxuhgr  47787  fldhmsubcALTV  48176  elbigolo1  48406  sepfsepc  48723