Theorem ssidd 4007

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3951

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

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

This theorem is referenced by:  funfvima2d  7252  suppofss1d  8229  suppofss2d  8230  fpr1  8328  ralxpmap  8936  fissuni  9397  fsuppssov1  9424  fsuppmptif  9439  fsuppco2  9443  fsuppcor  9444  mapfienlem1  9445  mapfienlem2  9446  cantnfp1lem1  9718  cantnfp1lem3  9720  cantnflem1  9729  htalem  9936  ackbij2lem4  10281  cflim2  10303  fin23lem15  10374  wunex2  10778  swrd0  14696  rtrclreclem1  15096  summolem3  15750  isum  15755  fsumser  15766  fsumcl  15769  flo1  15890  prodmolem3  15969  iprod  15974  iprodn0  15976  fprodss  15984  fprodcl  15988  fprodclf  16028  rpnnen2lem11  16260  eulerthlem2  16819  mremre  17647  catsubcat  17884  yon11  18309  yon12  18310  yon2  18311  yonpropd  18313  oppcyon  18314  yonffth  18329  submgmid  18719  submid  18823  mulgnncl  19107  mulgnn0cl  19108  mulgcl  19109  subgid  19146  snsymgefmndeq  19412  symggen  19488  gsumzcl2  19928  gsumzf1o  19930  gsum2dlem1  19988  gsum2dlem2  19989  gsum2d  19990  gsumxp2  19998  dprdfinv  20039  dmdprdsplitlem  20057  dprd2db  20063  dpjidcl  20078  ablfac1eu  20093  ablfaclem2  20106  gsumdixp  20316  subrngid  20549  rnghmsscmap2  20629  rhmsscmap2  20658  fldhmsubc  20786  primefld  20806  lcomfsupp  20900  lss1  20936  rlmbas  21200  rlmplusg  21201  rlm0  21202  rlmmulr  21204  rlmsca  21205  rlmsca2  21206  rlmvsca  21207  rlmtopn  21208  rlmds  21209  rng2idl1cntr  21315  regsumsupp  21640  frlmsslsp  21816  frlmup1  21818  rnasclassa  21915  mplsubglem  22019  mpllsslem  22020  mplsubrglem  22024  mplcoe1  22055  mplcoe5  22058  mplbas2  22060  evlslem4  22100  psrbagev1  22101  evlslem2  22103  mhpvscacl  22158  psdmplcl  22166  evls1fpws  22373  evl1maprhm  22383  mhmcompl  22384  mamures  22401  cpmadumatpolylem2  22888  neiptopuni  23138  neiptoptop  23139  restopn2  23185  rncmp  23404  cmpfi  23416  conncn  23434  llyidm  23496  nllyidm  23497  toplly  23498  kgentopon  23546  kgencn2  23565  ptcld  23621  qtopuni  23710  supnfcls  24028  utopbas  24244  metustfbas  24570  rrxcph  25426  rrxmval  25439  rrxdstprj1  25443  evthicc2  25495  volcn  25641  dvres3  25948  dvres3a  25949  dvidlem  25950  dvmptresicc  25951  dvcnp2  25955  dvnadd  25965  dvnres  25967  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcmul  25981  dvcmulf  25982  dvcobr  25983  dvcobrOLD  25984  dvcjbr  25987  dvrec  25993  dveflem  26017  dvef  26018  dvlipcn  26033  dvgt0lem2  26042  lhop1lem  26052  ftc1cn  26084  ftc2  26085  itgpowd  26091  deg1mul3le  26156  coeeulem  26263  dgrcolem1  26313  dgrcolem2  26314  plycpn  26331  dvntaylp  26413  pserdv  26473  pige3ALT  26562  cxpcn2  26789  rlimcnp3  27010  lgamgulmlem2  27073  basellem2  27125  pntrsumo1  27609  pntrsumbnd  27610  nosupbnd1lem1  27753  noinfbnd1lem1  27768  cutlt  27966  nbupgr  29361  nbumgrvtx  29363  nbgr2vtx1edg  29367  cusgrexilem2  29459  ifpsnprss  29641  1pthon2ve  30173  suppovss  32690  offinsupp1  32738  xrsmulgzz  33011  gsummpt2co  33051  gsumfs2d  33058  gsumpart  33060  gsumhashmul  33064  symgcom2  33104  pmtrcnelor  33111  tocycfvres1  33130  tocycfvres2  33131  cycpmconjvlem  33161  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnsubrunlem1  33251  fracf1  33309  idomsubr  33311  fldgenid  33321  lindfpropd  33410  lsmsnpridl  33426  qusrn  33437  elrspunidl  33456  ssdifidl  33485  mxidlprm  33498  ssmxidl  33502  rlmdim  33660  rgmoddimOLD  33661  tngdim  33664  matdim  33666  ply1degltdimlem  33673  fedgmullem1  33680  fldextrspunlsplem  33723  algextdeglem8  33765  constrmon  33785  mdetpmtr1  33822  zarclssn  33872  zart0  33878  zarcmplem  33880  pnfneige0  33950  pwsiga  34131  baselcarsg  34308  boolesineq  34457  efmul2picn  34611  reprfz1  34639  breprexplemc  34647  circlemeth  34655  circlevma  34657  circlemethhgt  34658  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  satfsschain  35369  mrsubff1  35519  mrsub0  35521  mrsubccat  35523  mrsubcn  35524  msubff1  35561  mthmpps  35587  wzel  35825  knoppndvlem6  36518  knoppndv  36535  bj-elpwg  37053  bj-restpw  37093  bj-restb  37095  bj-restuni2  37099  ftc1cnnclem  37698  ftc1cnnc  37699  ftc2nc  37709  areacirclem3  37717  welb  37743  cnresima  37771  rngoidl  38031  1psubclN  39946  cdlemefrs32fva  40402  lcmineqlem9  42038  lcmineqlem12  42041  intlewftc  42062  aks4d1p9  42089  primrootspoweq0  42107  sticksstones11  42157  aks6d1c6lem3  42173  aks6d1c6lem4  42174  aks6d1c6lem5  42178  aks6d1c7lem1  42181  addinvcom  42461  evlsvvvallem  42571  evlsvvvallem2  42572  evlsvvval  42573  selvcllem4  42591  selvvvval  42595  evlselv  42597  rgspnid  43180  oacl2g  43343  omabs2  43345  omcl2  43346  tfsconcatb0  43357  naddgeoa  43407  harval3  43551  cnvtrucl0  43637  brfvrtrcld  43747  clsk3nimkb  44053  k0004ss2  44165  extoimad  44177  mnuprd  44295  dvconstbi  44353  ssinc  45092  ssdec  45093  restopn3  45156  founiiun  45184  choicefi  45205  islptre  45634  fnlimfvre  45689  addccncf2  45891  fsumcncf  45893  cncfperiod  45894  negcncfg  45896  cncfuni  45901  icccncfext  45902  cncficcgt0  45903  fprodcncf  45915  dvcnre  45931  fperdvper  45934  itgsinexplem1  45969  itgcoscmulx  45984  smfpimne2  46855  predgclnbgrel  47825  isubgrvtxuhgr  47850  fldhmsubcALTV  48249  elbigolo1  48478  sepfsepc  48825