Theorem ssidd 3924

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  funfvima2d  7048  suppofss1d  7946  suppofss2d  7947  fpr1  8043  ralxpmap  8577  fissuni  8981  fsuppmptif  9015  fsuppco2  9019  fsuppcor  9020  mapfienlem1  9021  mapfienlem2  9022  cantnfp1lem1  9293  cantnfp1lem3  9295  cantnflem1  9304  trpredpo  9341  htalem  9512  ackbij2lem4  9856  cflim2  9877  fin23lem15  9948  wunex2  10352  swrd0  14223  rtrclreclem1  14620  summolem3  15278  isum  15283  fsumser  15294  fsumcl  15297  flo1  15418  prodmolem3  15495  iprod  15500  iprodn0  15502  fprodss  15510  fprodcl  15514  fprodclf  15554  rpnnen2lem11  15785  eulerthlem2  16335  mremre  17107  catsubcat  17345  yon11  17772  yon12  17773  yon2  17774  yonpropd  17776  oppcyon  17777  yonffth  17792  submid  18237  mulgnncl  18507  mulgnn0cl  18508  mulgcl  18509  subgid  18545  snsymgefmndeq  18787  symggen  18862  gsumzcl2  19295  gsumzf1o  19297  gsum2dlem1  19355  gsum2dlem2  19356  gsum2d  19357  gsumxp2  19365  dprdfinv  19406  dmdprdsplitlem  19424  dprd2db  19430  dpjidcl  19445  ablfac1eu  19460  ablfaclem2  19473  gsumdixp  19627  primefld  19849  lcomfsupp  19939  lss1  19975  rlmbas  20232  rlmplusg  20233  rlm0  20234  rlmmulr  20236  rlmsca  20237  rlmsca2  20238  rlmvsca  20239  rlmtopn  20240  rlmds  20241  regsumsupp  20584  frlmsslsp  20758  frlmup1  20760  rnasclassa  20855  mplsubglem  20961  mpllsslem  20962  mplsubrglem  20966  mplcoe1  20994  mplcoe5  20997  mplbas2  20999  evlslem4  21034  psrbagev1  21035  psrbagev1OLD  21036  evlslem2  21039  mhpvscacl  21094  mamures  21289  cpmadumatpolylem2  21779  neiptopuni  22027  neiptoptop  22028  restopn2  22074  rncmp  22293  cmpfi  22305  conncn  22323  llyidm  22385  nllyidm  22386  toplly  22387  kgentopon  22435  kgencn2  22454  ptcld  22510  qtopuni  22599  supnfcls  22917  utopbas  23133  metustfbas  23455  rrxcph  24289  rrxmval  24302  rrxdstprj1  24306  evthicc2  24357  volcn  24503  dvres3  24810  dvres3a  24811  dvidlem  24812  dvmptresicc  24813  dvnadd  24826  dvnres  24828  dvaddbr  24835  dvmulbr  24836  dvcmul  24841  dvcmulf  24842  dvcobr  24843  dvcjbr  24846  dvrec  24852  dveflem  24876  dvef  24877  dvlipcn  24891  dvgt0lem2  24900  lhop1lem  24910  ftc1cn  24940  ftc2  24941  itgpowd  24947  deg1mul3le  25014  coeeulem  25118  dgrcolem1  25167  dgrcolem2  25168  plycpn  25182  dvntaylp  25263  pserdv  25321  pige3ALT  25409  cxpcn2  25632  rlimcnp3  25850  lgamgulmlem2  25912  basellem2  25964  pntrsumo1  26446  pntrsumbnd  26447  nbupgr  27432  nbumgrvtx  27434  nbgr2vtx1edg  27438  cusgrexilem2  27530  ifpsnprss  27710  1pthon2ve  28237  suppovss  30737  offinsupp1  30782  xrsmulgzz  31006  gsummpt2co  31027  gsumpart  31034  gsumhashmul  31035  symgcom2  31072  pmtrcnelor  31079  tocycfvres1  31096  tocycfvres2  31097  cycpmconjvlem  31127  lindfpropd  31290  lsmsnpridl  31300  elrspunidl  31320  mxidlprm  31354  ssmxidl  31356  rgmoddim  31407  tngdim  31410  matdim  31412  fedgmullem1  31424  mdetpmtr1  31487  zarclssn  31537  zart0  31543  zarcmplem  31545  pnfneige0  31615  pwsiga  31810  baselcarsg  31985  efmul2picn  32288  reprfz1  32316  breprexplemc  32324  circlemeth  32332  circlevma  32334  circlemethhgt  32335  hgt750lemb  32348  hgt750lema  32349  hgt750leme  32350  tgoldbachgtde  32352  satfsschain  33039  mrsubff1  33189  mrsub0  33191  mrsubccat  33193  mrsubcn  33194  msubff1  33231  mthmpps  33257  wzel  33555  nosupbnd1lem1  33648  noinfbnd1lem1  33663  knoppndvlem6  34434  knoppndv  34451  bj-elpwg  34962  bj-restpw  34998  bj-restb  35000  bj-restuni2  35004  ftc1cnnclem  35585  ftc1cnnc  35586  ftc2nc  35596  areacirclem3  35604  welb  35631  cnresima  35659  rngoidl  35919  1psubclN  37695  cdlemefrs32fva  38151  lcmineqlem9  39779  lcmineqlem12  39782  intlewftc  39803  sticksstones11  39834  selvval2lem4  39941  evlsbagval  39985  mhphf  39995  addinvcom  40121  rgspnid  40700  harval3  40828  cnvtrucl0  40908  brfvrtrcld  41019  clsk3nimkb  41327  k0004ss2  41439  extoimad  41452  mnuprd  41567  dvconstbi  41625  ssinc  42310  ssdec  42311  founiiun  42388  choicefi  42413  islptre  42835  fnlimfvre  42890  addccncf2  43092  fsumcncf  43094  cncfperiod  43095  negcncfg  43097  cncfuni  43102  icccncfext  43103  cncficcgt0  43104  fprodcncf  43116  dvcnre  43132  fperdvper  43135  itgsinexplem1  43170  itgcoscmulx  43185  submgmid  45020  rnghmsscmap2  45204  rhmsscmap2  45250  fldhmsubc  45315  fldhmsubcALTV  45333  elbigolo1  45576  sepfsepc  45894