Theorem ssidd 3956

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3900

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

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

This theorem is referenced by:  funfvima2d  7161  suppofss1d  8129  suppofss2d  8130  fpr1  8228  ralxpmap  8815  fissuni  9236  fsuppssov1  9263  fsuppmptif  9278  fsuppco2  9282  fsuppcor  9283  mapfienlem1  9284  mapfienlem2  9285  cantnfp1lem1  9563  cantnfp1lem3  9565  cantnflem1  9574  htalem  9781  ackbij2lem4  10124  cflim2  10146  fin23lem15  10217  wunex2  10621  swrd0  14558  rtrclreclem1  14956  summolem3  15613  isum  15618  fsumser  15629  fsumcl  15632  flo1  15753  prodmolem3  15832  iprod  15837  iprodn0  15839  fprodss  15847  fprodcl  15851  fprodclf  15891  rpnnen2lem11  16125  eulerthlem2  16685  mremre  17498  catsubcat  17738  yon11  18162  yon12  18163  yon2  18164  yonpropd  18166  oppcyon  18167  yonffth  18182  submgmid  18606  submid  18710  mulgnncl  18994  mulgnn0cl  18995  mulgcl  18996  subgid  19033  snsymgefmndeq  19300  symggen  19375  gsumzcl2  19815  gsumzf1o  19817  gsum2dlem1  19875  gsum2dlem2  19876  gsum2d  19877  gsumxp2  19885  dprdfinv  19926  dmdprdsplitlem  19944  dprd2db  19950  dpjidcl  19965  ablfac1eu  19980  ablfaclem2  19993  gsumdixp  20230  subrngid  20457  rnghmsscmap2  20537  rhmsscmap2  20566  fldhmsubc  20693  primefld  20713  lcomfsupp  20828  lss1  20864  rlmbas  21120  rlmplusg  21121  rlm0  21122  rlmmulr  21124  rlmsca  21125  rlmsca2  21126  rlmvsca  21127  rlmtopn  21128  rlmds  21129  rng2idl1cntr  21235  regsumsupp  21552  frlmsslsp  21726  frlmup1  21728  rnasclassa  21825  mplsubglem  21929  mpllsslem  21930  mplsubrglem  21934  mplcoe1  21965  mplcoe5  21968  mplbas2  21970  evlslem4  22004  psrbagev1  22005  evlslem2  22007  mhpvscacl  22062  psdmplcl  22070  evls1fpws  22277  evl1maprhm  22287  mhmcompl  22288  mamures  22305  cpmadumatpolylem2  22790  neiptopuni  23038  neiptoptop  23039  restopn2  23085  rncmp  23304  cmpfi  23316  conncn  23334  llyidm  23396  nllyidm  23397  toplly  23398  kgentopon  23446  kgencn2  23465  ptcld  23521  qtopuni  23610  supnfcls  23928  utopbas  24143  metustfbas  24465  rrxcph  25312  rrxmval  25325  rrxdstprj1  25329  evthicc2  25381  volcn  25527  dvres3  25834  dvres3a  25835  dvidlem  25836  dvmptresicc  25837  dvcnp2  25841  dvnadd  25851  dvnres  25853  dvaddbr  25860  dvmulbr  25861  dvmulbrOLD  25862  dvcmul  25867  dvcmulf  25868  dvcobr  25869  dvcobrOLD  25870  dvcjbr  25873  dvrec  25879  dveflem  25903  dvef  25904  dvlipcn  25919  dvgt0lem2  25928  lhop1lem  25938  ftc1cn  25970  ftc2  25971  itgpowd  25977  deg1mul3le  26042  coeeulem  26149  dgrcolem1  26199  dgrcolem2  26200  plycpn  26217  dvntaylp  26299  pserdv  26359  pige3ALT  26449  cxpcn2  26676  rlimcnp3  26897  lgamgulmlem2  26960  basellem2  27012  pntrsumo1  27496  pntrsumbnd  27497  nosupbnd1lem1  27640  noinfbnd1lem1  27655  cutlt  27869  nbupgr  29315  nbumgrvtx  29317  nbgr2vtx1edg  29321  cusgrexilem2  29413  ifpsnprss  29594  1pthon2ve  30124  suppovss  32652  offinsupp1  32699  xrsmulgzz  32980  gsummpt2co  33018  gsumfs2d  33025  gsumpart  33027  gsumhashmul  33031  symgcom2  33043  pmtrcnelor  33050  tocycfvres1  33069  tocycfvres2  33070  cycpmconjvlem  33100  elrgspnlem1  33199  elrgspnlem2  33200  elrgspnsubrunlem1  33204  fracf1  33263  idomsubr  33265  fldgenid  33275  lindfpropd  33337  lsmsnpridl  33353  qusrn  33364  elrspunidl  33383  ssdifidl  33412  mxidlprm  33425  ssmxidl  33429  mplvrpmrhm  33567  srapwov  33591  rlmdim  33612  rgmoddimOLD  33613  tngdim  33616  matdim  33618  ply1degltdimlem  33625  fedgmullem1  33632  fldextrspunlsplem  33676  algextdeglem8  33727  constrmon  33747  mdetpmtr1  33826  zarclssn  33876  zart0  33882  zarcmplem  33884  pnfneige0  33954  pwsiga  34133  baselcarsg  34309  boolesineq  34458  efmul2picn  34599  reprfz1  34627  breprexplemc  34635  circlemeth  34643  circlevma  34645  circlemethhgt  34646  hgt750lemb  34659  hgt750lema  34660  hgt750leme  34661  tgoldbachgtde  34663  satfsschain  35376  mrsubff1  35526  mrsub0  35528  mrsubccat  35530  mrsubcn  35531  msubff1  35568  mthmpps  35594  wzel  35837  knoppndvlem6  36530  knoppndv  36547  bj-elpwg  37065  bj-restpw  37105  bj-restb  37107  bj-restuni2  37111  ftc1cnnclem  37710  ftc1cnnc  37711  ftc2nc  37721  areacirclem3  37729  welb  37755  cnresima  37783  rngoidl  38043  1psubclN  39962  cdlemefrs32fva  40418  lcmineqlem9  42049  lcmineqlem12  42052  intlewftc  42073  aks4d1p9  42100  primrootspoweq0  42118  sticksstones11  42168  aks6d1c6lem3  42184  aks6d1c6lem4  42185  aks6d1c6lem5  42189  aks6d1c7lem1  42192  addinvcom  42444  evlsvvvallem  42573  evlsvvvallem2  42574  evlsvvval  42575  selvcllem4  42593  selvvvval  42597  evlselv  42599  rgspnid  43180  oacl2g  43342  omabs2  43344  omcl2  43345  tfsconcatb0  43356  naddgeoa  43406  harval3  43550  cnvtrucl0  43636  brfvrtrcld  43746  clsk3nimkb  44052  k0004ss2  44164  extoimad  44176  mnuprd  44288  dvconstbi  44346  ssinc  45103  ssdec  45104  restopn3  45167  founiiun  45195  choicefi  45216  islptre  45638  fnlimfvre  45691  addccncf2  45893  fsumcncf  45895  cncfperiod  45896  negcncfg  45898  cncfuni  45903  icccncfext  45904  cncficcgt0  45905  fprodcncf  45917  dvcnre  45933  fperdvper  45936  itgsinexplem1  45971  itgcoscmulx  45986  smfpimne2  46857  predgclnbgrel  47849  isubgrvtxuhgr  47874  fldhmsubcALTV  48343  elbigolo1  48568  iunlub  48831  iinglb  48832  sepfsepc  48938