Theorem ssidd 3954

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3899

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

This theorem depends on definitions:  df-bi 209  df-ss 3916

This theorem is referenced by:  pwidg  4569  funfvima2d  7205  suppofss1d  8172  suppofss2d  8173  fpr1  8272  ralxpmap  8867  fissuni  9290  fsuppssov1  9320  fsuppmptif  9335  fsuppco2  9339  fsuppcor  9340  mapfienlem1  9341  mapfienlem2  9342  cantnfp1lem1  9623  cantnfp1lem3  9625  cantnflem1  9634  htalem  9844  ackbij2lem4  10187  cflim2  10210  fin23lem15  10281  wunex2  10686  swrd0  14662  rtrclreclem1  15060  summolem3  15717  isum  15722  fsumser  15733  fsumcl  15736  flo1  15860  prodmolem3  15939  iprod  15944  iprodn0  15946  fprodss  15954  fprodcl  15958  fprodclf  15998  rpnnen2lem11  16232  eulerthlem2  16793  mremre  17608  catsubcat  17848  yon11  18272  yon12  18273  yon2  18274  yonpropd  18276  oppcyon  18277  yonffth  18292  submgmid  18716  submid  18820  mulgnncl  19107  mulgnn0cl  19108  mulgcl  19109  subgid  19146  snsymgefmndeq  19411  symggen  19486  gsumzcl2  19926  gsumzf1o  19928  gsum2dlem1  19986  gsum2dlem2  19987  gsum2d  19988  gsumxp2  19996  dprdfinv  20037  dmdprdsplitlem  20055  dprd2db  20061  dpjidcl  20076  ablfac1eu  20091  ablfaclem2  20104  gsumdixp  20339  subrngid  20571  rnghmsscmap2  20651  rhmsscmap2  20680  fldhmsubc  20807  primefld  20827  lcomfsupp  20942  lss1  20978  rlmbas  21233  rlmplusg  21234  rlm0  21235  rlmmulr  21237  rlmsca  21238  rlmsca2  21239  rlmvsca  21240  rlmtopn  21241  rlmds  21242  rng2idl1cntr  21348  regsumsupp  21647  frlmsslsp  21821  frlmup1  21823  rnasclassa  21920  mplsubglem  22023  mpllsslem  22024  mplsubrglem  22028  mplcoe1  22063  mplcoe5  22066  mplbas2  22068  evlslem4  22102  psrbagev1  22103  evlslem2  22105  evlsvvvallem  22117  evlsvvvallem2  22118  evlsvvval  22119  mhmcompl  22147  selvcllem4  22164  selvvvval  22168  mhpvscacl  22192  psdmplcl  22200  evls1fpws  22405  evl1maprhm  22415  mamures  22430  cpmadumatpolylem2  22915  neiptopuni  23163  neiptoptop  23164  restopn2  23210  rncmp  23429  cmpfi  23441  conncn  23459  llyidm  23521  nllyidm  23522  toplly  23523  kgentopon  23571  kgencn2  23590  ptcld  23646  qtopuni  23735  supnfcls  24053  utopbas  24268  metustfbas  24590  rrxcph  25427  rrxmval  25440  rrxdstprj1  25444  evthicc2  25495  volcn  25641  dvres3  25948  dvres3a  25949  dvidlem  25950  dvmptresicc  25951  dvcnp2  25955  dvnadd  25964  dvnres  25966  dvaddbr  25973  dvmulbr  25974  dvcmul  25979  dvcmulf  25980  dvcobr  25981  dvcjbr  25984  dvrec  25990  dveflem  26014  dvef  26015  dvlipcn  26029  dvgt0lem2  26038  lhop1lem  26048  ftc1cn  26078  ftc2  26079  itgpowd  26085  deg1mul3le  26150  coeeulem  26257  dgrcolem1  26306  dgrcolem2  26307  plycpn  26323  dvntaylp  26404  pserdv  26462  pige3ALT  26555  cxpcn2  26781  rlimcnp3  27002  lgamgulmlem2  27064  basellem2  27116  pntrsumo1  27599  pntrsumbnd  27600  nosupbnd1lem1  27742  noinfbnd1lem1  27757  cutlt  27995  nbupgr  29484  nbumgrvtx  29486  nbgr2vtx1edg  29490  cusgrexilem2  29582  ifpsnprss  29762  1pthon2ve  30295  suppovss  32826  offinsupp1  32871  xrsmulgzz  33141  gsummpt2co  33182  gsummptrev  33190  gsummptp1  33191  gsumfs2d  33195  gsumpart  33197  gsumhashmul  33201  gsummulsubdishift1  33202  symgcom2  33218  pmtrcnelor  33225  tocycfvres1  33244  tocycfvres2  33245  cycpmconjvlem  33275  elrgspnlem1  33377  elrgspnlem2  33378  elrgspnsubrunlem1  33382  fracf1  33448  idomsubr  33450  fldgenid  33460  lindfpropd  33522  lsmsnpridl  33538  qusrn  33549  elrspunidl  33568  ssdifidl  33598  mxidlprm  33612  ssmxidl  33616  selvply1rhmlemb  33770  evlextv  33793  mplvrpmrhm  33798  vieta  33831  srapwov  33840  rlmdim  33861  tngdim  33864  matdim  33866  ply1degltdimlem  33873  fedgmullem1  33880  fldextrspunlsplem  33924  algextdeglem8  33975  constrmon  33995  mdetpmtr1  34074  zarclssn  34124  zart0  34130  zarcmplem  34132  pnfneige0  34202  pwsiga  34381  baselcarsg  34557  boolesineq  34706  efmul2picn  34847  reprfz1  34875  breprexplemc  34883  circlemeth  34891  circlevma  34893  circlemethhgt  34894  hgt750lemb  34907  hgt750lema  34908  hgt750leme  34909  tgoldbachgtde  34911  satfsschain  35662  mrsubff1  35812  mrsub0  35814  mrsubccat  35816  mrsubcn  35817  msubff1  35854  mthmpps  35880  wzel  36120  nmulprop  36488  knoppndvlem6  36903  knoppndv  36920  bj-elpwg  37485  bj-restpw  37530  bj-restb  37532  bj-restuni2  37536  ftc1cnnclem  38138  ftc1cnnc  38139  ftc2nc  38149  areacirclem3  38157  welb  38183  cnresima  38211  rngoidl  38471  1psubclN  40516  cdlemefrs32fva  40972  lcmineqlem9  42602  lcmineqlem12  42605  intlewftc  42626  aks4d1p9  42653  primrootspoweq0  42671  sticksstones11  42721  aks6d1c6lem3  42737  aks6d1c6lem4  42738  aks6d1c6lem5  42742  aks6d1c7lem1  42745  addinvcom  42989  evlselv  43119  rgspnid  43693  oacl2g  43855  omabs2  43857  omcl2  43858  tfsconcatb0  43869  naddgeoa  43919  harval3  44062  cnvtrucl0  44148  brfvrtrcld  44258  clsk3nimkb  44564  k0004ss2  44676  extoimad  44688  mnuprd  44800  dvconstbi  44858  ssinc  45613  ssdec  45614  restopn3  45677  founiiun  45705  choicefi  45725  islptre  46143  fnlimfvre  46196  addccncf2  46398  fsumcncf  46400  cncfperiod  46401  negcncfg  46403  cncfuni  46408  icccncfext  46409  cncficcgt0  46410  fprodcncf  46422  dvcnre  46438  fperdvper  46441  itgsinexplem1  46476  itgcoscmulx  46491  smfpimne2  47362  predgclnbgrel  48409  isubgrvtxuhgr  48434  fldhmsubcALTV  48903  elbigolo1  49127  iunlub  49390  iinglb  49391  sepfsepc  49497