Theorem ssidd 3990

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  funfvima2d  6994  suppofss1d  7868  suppofss2d  7869  ralxpmap  8460  fissuni  8829  fsuppmptif  8863  fsuppco2  8866  fsuppcor  8867  mapfienlem1  8868  mapfienlem2  8869  cantnfp1lem1  9141  cantnfp1lem3  9143  cantnflem1  9152  htalem  9325  ackbij2lem4  9664  cflim2  9685  fin23lem15  9756  wunex2  10160  swrd0  14020  rtrclreclem2  14418  summolem3  15071  isum  15076  fsumser  15087  fsumcl  15090  flo1  15209  prodmolem3  15287  iprod  15292  iprodn0  15294  fprodss  15302  fprodcl  15306  fprodclf  15346  rpnnen2lem11  15577  eulerthlem2  16119  mremre  16875  catsubcat  17109  yon11  17514  yon12  17515  yon2  17516  yonpropd  17518  oppcyon  17519  yonffth  17534  submid  17975  mulgnncl  18243  mulgnn0cl  18244  mulgcl  18245  subgid  18281  snsymgefmndeq  18523  symggen  18598  gsumzcl2  19030  gsumzf1o  19032  gsum2dlem1  19090  gsum2dlem2  19091  gsum2d  19092  gsumxp2  19100  dprdfinv  19141  dmdprdsplitlem  19159  dprd2db  19165  dpjidcl  19180  ablfac1eu  19195  ablfaclem2  19208  gsumdixp  19359  primefld  19584  lcomfsupp  19674  lss1  19710  rlmbas  19967  rlmplusg  19968  rlm0  19969  rlmmulr  19971  rlmsca  19972  rlmsca2  19973  rlmvsca  19974  rlmtopn  19975  rlmds  19976  rnasclassa  20124  mplsubglem  20214  mpllsslem  20215  mplsubrglem  20219  mplcoe1  20246  mplcoe5  20249  mplbas2  20251  evlslem4  20288  psrbagev1  20290  evlslem2  20292  mhpvscacl  20341  regsumsupp  20766  frlmsslsp  20940  frlmup1  20942  mamures  21001  cpmadumatpolylem2  21490  neiptopuni  21738  neiptoptop  21739  restopn2  21785  rncmp  22004  cmpfi  22016  conncn  22034  llyidm  22096  nllyidm  22097  toplly  22098  kgentopon  22146  kgencn2  22165  ptcld  22221  qtopuni  22310  supnfcls  22628  utopbas  22844  metustfbas  23167  rrxcph  23995  rrxmval  24008  rrxdstprj1  24012  evthicc2  24061  volcn  24207  dvres3  24511  dvres3a  24512  dvidlem  24513  dvnadd  24526  dvnres  24528  dvaddbr  24535  dvmulbr  24536  dvcmul  24541  dvcmulf  24542  dvcobr  24543  dvcjbr  24546  dvrec  24552  dveflem  24576  dvef  24577  dvlipcn  24591  dvgt0lem2  24600  lhop1lem  24610  ftc1cn  24640  ftc2  24641  deg1mul3le  24710  coeeulem  24814  dgrcolem1  24863  dgrcolem2  24864  plycpn  24878  dvntaylp  24959  pserdv  25017  pige3ALT  25105  cxpcn2  25327  rlimcnp3  25545  lgamgulmlem2  25607  basellem2  25659  pntrsumo1  26141  pntrsumbnd  26142  nbupgr  27126  nbumgrvtx  27128  nbgr2vtx1edg  27132  cusgrexilem2  27224  ifpsnprss  27404  1pthon2ve  27933  suppovss  30426  offinsupp1  30463  xrsmulgzz  30665  gsummpt2co  30686  symgcom2  30728  pmtrcnelor  30735  tocycfvres1  30752  tocycfvres2  30753  cycpmconjvlem  30783  lindfpropd  30942  lsmsnpridl  30948  mxidlprm  30977  ssmxidl  30979  rgmoddim  31008  tngdim  31011  matdim  31013  fedgmullem1  31025  mdetpmtr1  31088  pnfneige0  31194  pwsiga  31389  baselcarsg  31564  efmul2picn  31867  reprfz1  31895  breprexplemc  31903  circlemeth  31911  circlevma  31913  circlemethhgt  31914  hgt750lemb  31927  hgt750lema  31928  hgt750leme  31929  tgoldbachgtde  31931  satfsschain  32611  mrsubff1  32761  mrsub0  32763  mrsubccat  32765  mrsubcn  32766  msubff1  32803  mthmpps  32829  trpredpo  33074  wzel  33111  fpr1  33139  nosupbnd1lem1  33208  knoppndvlem6  33856  knoppndv  33873  bj-elpwg  34348  bj-restpw  34386  bj-restb  34388  bj-restuni2  34392  ftc1cnnclem  34980  ftc1cnnc  34981  ftc2nc  34991  areacirclem3  34999  welb  35026  cnresima  35057  rngoidl  35317  1psubclN  37095  cdlemefrs32fva  37551  selvval2lem4  39185  rgspnid  39821  itgpowd  39870  harval3  39953  cnvtrucl0  40033  brfvrtrcld  40128  clsk3nimkb  40439  k0004ss2  40551  extoimad  40564  mnuprd  40661  dvconstbi  40715  ssinc  41402  ssdec  41403  founiiun  41484  choicefi  41512  islptre  41949  fnlimfvre  42004  addccncf2  42208  fsumcncf  42210  cncfperiod  42211  negcncfg  42213  cncfuni  42218  icccncfext  42219  cncficcgt0  42220  fprodcncf  42233  dvcnre  42249  fperdvper  42252  dvmptresicc  42253  itgsinexplem1  42288  itgcoscmulx  42303  submgmid  44109  rnghmsscmap2  44293  rhmsscmap2  44339  fldhmsubc  44404  fldhmsubcALTV  44422  elbigolo1  44666