Theorem ssidd 3973

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3917

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 3934

This theorem is referenced by:  funfvima2d  7209  suppofss1d  8186  suppofss2d  8187  fpr1  8285  ralxpmap  8872  fissuni  9315  fsuppssov1  9342  fsuppmptif  9357  fsuppco2  9361  fsuppcor  9362  mapfienlem1  9363  mapfienlem2  9364  cantnfp1lem1  9638  cantnfp1lem3  9640  cantnflem1  9649  htalem  9856  ackbij2lem4  10201  cflim2  10223  fin23lem15  10294  wunex2  10698  swrd0  14630  rtrclreclem1  15030  summolem3  15687  isum  15692  fsumser  15703  fsumcl  15706  flo1  15827  prodmolem3  15906  iprod  15911  iprodn0  15913  fprodss  15921  fprodcl  15925  fprodclf  15965  rpnnen2lem11  16199  eulerthlem2  16759  mremre  17572  catsubcat  17808  yon11  18232  yon12  18233  yon2  18234  yonpropd  18236  oppcyon  18237  yonffth  18252  submgmid  18640  submid  18744  mulgnncl  19028  mulgnn0cl  19029  mulgcl  19030  subgid  19067  snsymgefmndeq  19332  symggen  19407  gsumzcl2  19847  gsumzf1o  19849  gsum2dlem1  19907  gsum2dlem2  19908  gsum2d  19909  gsumxp2  19917  dprdfinv  19958  dmdprdsplitlem  19976  dprd2db  19982  dpjidcl  19997  ablfac1eu  20012  ablfaclem2  20025  gsumdixp  20235  subrngid  20465  rnghmsscmap2  20545  rhmsscmap2  20574  fldhmsubc  20701  primefld  20721  lcomfsupp  20815  lss1  20851  rlmbas  21107  rlmplusg  21108  rlm0  21109  rlmmulr  21111  rlmsca  21112  rlmsca2  21113  rlmvsca  21114  rlmtopn  21115  rlmds  21116  rng2idl1cntr  21222  regsumsupp  21538  frlmsslsp  21712  frlmup1  21714  rnasclassa  21811  mplsubglem  21915  mpllsslem  21916  mplsubrglem  21920  mplcoe1  21951  mplcoe5  21954  mplbas2  21956  evlslem4  21990  psrbagev1  21991  evlslem2  21993  mhpvscacl  22048  psdmplcl  22056  evls1fpws  22263  evl1maprhm  22273  mhmcompl  22274  mamures  22291  cpmadumatpolylem2  22776  neiptopuni  23024  neiptoptop  23025  restopn2  23071  rncmp  23290  cmpfi  23302  conncn  23320  llyidm  23382  nllyidm  23383  toplly  23384  kgentopon  23432  kgencn2  23451  ptcld  23507  qtopuni  23596  supnfcls  23914  utopbas  24130  metustfbas  24452  rrxcph  25299  rrxmval  25312  rrxdstprj1  25316  evthicc2  25368  volcn  25514  dvres3  25821  dvres3a  25822  dvidlem  25823  dvmptresicc  25824  dvcnp2  25828  dvnadd  25838  dvnres  25840  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcmul  25854  dvcmulf  25855  dvcobr  25856  dvcobrOLD  25857  dvcjbr  25860  dvrec  25866  dveflem  25890  dvef  25891  dvlipcn  25906  dvgt0lem2  25915  lhop1lem  25925  ftc1cn  25957  ftc2  25958  itgpowd  25964  deg1mul3le  26029  coeeulem  26136  dgrcolem1  26186  dgrcolem2  26187  plycpn  26204  dvntaylp  26286  pserdv  26346  pige3ALT  26436  cxpcn2  26663  rlimcnp3  26884  lgamgulmlem2  26947  basellem2  26999  pntrsumo1  27483  pntrsumbnd  27484  nosupbnd1lem1  27627  noinfbnd1lem1  27642  cutlt  27847  nbupgr  29278  nbumgrvtx  29280  nbgr2vtx1edg  29284  cusgrexilem2  29376  ifpsnprss  29558  1pthon2ve  30090  suppovss  32611  offinsupp1  32657  xrsmulgzz  32954  gsummpt2co  32995  gsumfs2d  33002  gsumpart  33004  gsumhashmul  33008  symgcom2  33048  pmtrcnelor  33055  tocycfvres1  33074  tocycfvres2  33075  cycpmconjvlem  33105  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnsubrunlem1  33205  fracf1  33264  idomsubr  33266  fldgenid  33276  lindfpropd  33360  lsmsnpridl  33376  qusrn  33387  elrspunidl  33406  ssdifidl  33435  mxidlprm  33448  ssmxidl  33452  rlmdim  33612  rgmoddimOLD  33613  tngdim  33616  matdim  33618  ply1degltdimlem  33625  fedgmullem1  33632  fldextrspunlsplem  33675  algextdeglem8  33721  constrmon  33741  mdetpmtr1  33820  zarclssn  33870  zart0  33876  zarcmplem  33878  pnfneige0  33948  pwsiga  34127  baselcarsg  34304  boolesineq  34453  efmul2picn  34594  reprfz1  34622  breprexplemc  34630  circlemeth  34638  circlevma  34640  circlemethhgt  34641  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  tgoldbachgtde  34658  satfsschain  35358  mrsubff1  35508  mrsub0  35510  mrsubccat  35512  mrsubcn  35513  msubff1  35550  mthmpps  35576  wzel  35819  knoppndvlem6  36512  knoppndv  36529  bj-elpwg  37047  bj-restpw  37087  bj-restb  37089  bj-restuni2  37093  ftc1cnnclem  37692  ftc1cnnc  37693  ftc2nc  37703  areacirclem3  37711  welb  37737  cnresima  37765  rngoidl  38025  1psubclN  39945  cdlemefrs32fva  40401  lcmineqlem9  42032  lcmineqlem12  42035  intlewftc  42056  aks4d1p9  42083  primrootspoweq0  42101  sticksstones11  42151  aks6d1c6lem3  42167  aks6d1c6lem4  42168  aks6d1c6lem5  42172  aks6d1c7lem1  42175  addinvcom  42427  evlsvvvallem  42556  evlsvvvallem2  42557  evlsvvval  42558  selvcllem4  42576  selvvvval  42580  evlselv  42582  rgspnid  43164  oacl2g  43326  omabs2  43328  omcl2  43329  tfsconcatb0  43340  naddgeoa  43390  harval3  43534  cnvtrucl0  43620  brfvrtrcld  43730  clsk3nimkb  44036  k0004ss2  44148  extoimad  44160  mnuprd  44272  dvconstbi  44330  ssinc  45088  ssdec  45089  restopn3  45152  founiiun  45180  choicefi  45201  islptre  45624  fnlimfvre  45679  addccncf2  45881  fsumcncf  45883  cncfperiod  45884  negcncfg  45886  cncfuni  45891  icccncfext  45892  cncficcgt0  45893  fprodcncf  45905  dvcnre  45921  fperdvper  45924  itgsinexplem1  45959  itgcoscmulx  45974  smfpimne2  46845  predgclnbgrel  47843  isubgrvtxuhgr  47868  fldhmsubcALTV  48325  elbigolo1  48550  iunlub  48813  iinglb  48814  sepfsepc  48920