Theorem ssidd 3961

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3905

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 3922

This theorem is referenced by:  funfvima2d  7172  suppofss1d  8144  suppofss2d  8145  fpr1  8243  ralxpmap  8830  fissuni  9266  fsuppssov1  9293  fsuppmptif  9308  fsuppco2  9312  fsuppcor  9313  mapfienlem1  9314  mapfienlem2  9315  cantnfp1lem1  9593  cantnfp1lem3  9595  cantnflem1  9604  htalem  9811  ackbij2lem4  10154  cflim2  10176  fin23lem15  10247  wunex2  10651  swrd0  14583  rtrclreclem1  14982  summolem3  15639  isum  15644  fsumser  15655  fsumcl  15658  flo1  15779  prodmolem3  15858  iprod  15863  iprodn0  15865  fprodss  15873  fprodcl  15877  fprodclf  15917  rpnnen2lem11  16151  eulerthlem2  16711  mremre  17524  catsubcat  17764  yon11  18188  yon12  18189  yon2  18190  yonpropd  18192  oppcyon  18193  yonffth  18208  submgmid  18598  submid  18702  mulgnncl  18986  mulgnn0cl  18987  mulgcl  18988  subgid  19025  snsymgefmndeq  19292  symggen  19367  gsumzcl2  19807  gsumzf1o  19809  gsum2dlem1  19867  gsum2dlem2  19868  gsum2d  19869  gsumxp2  19877  dprdfinv  19918  dmdprdsplitlem  19936  dprd2db  19942  dpjidcl  19957  ablfac1eu  19972  ablfaclem2  19985  gsumdixp  20222  subrngid  20452  rnghmsscmap2  20532  rhmsscmap2  20561  fldhmsubc  20688  primefld  20708  lcomfsupp  20823  lss1  20859  rlmbas  21115  rlmplusg  21116  rlm0  21117  rlmmulr  21119  rlmsca  21120  rlmsca2  21121  rlmvsca  21122  rlmtopn  21123  rlmds  21124  rng2idl1cntr  21230  regsumsupp  21547  frlmsslsp  21721  frlmup1  21723  rnasclassa  21820  mplsubglem  21924  mpllsslem  21925  mplsubrglem  21929  mplcoe1  21960  mplcoe5  21963  mplbas2  21965  evlslem4  21999  psrbagev1  22000  evlslem2  22002  mhpvscacl  22057  psdmplcl  22065  evls1fpws  22272  evl1maprhm  22282  mhmcompl  22283  mamures  22300  cpmadumatpolylem2  22785  neiptopuni  23033  neiptoptop  23034  restopn2  23080  rncmp  23299  cmpfi  23311  conncn  23329  llyidm  23391  nllyidm  23392  toplly  23393  kgentopon  23441  kgencn2  23460  ptcld  23516  qtopuni  23605  supnfcls  23923  utopbas  24139  metustfbas  24461  rrxcph  25308  rrxmval  25321  rrxdstprj1  25325  evthicc2  25377  volcn  25523  dvres3  25830  dvres3a  25831  dvidlem  25832  dvmptresicc  25833  dvcnp2  25837  dvnadd  25847  dvnres  25849  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvcmul  25863  dvcmulf  25864  dvcobr  25865  dvcobrOLD  25866  dvcjbr  25869  dvrec  25875  dveflem  25899  dvef  25900  dvlipcn  25915  dvgt0lem2  25924  lhop1lem  25934  ftc1cn  25966  ftc2  25967  itgpowd  25973  deg1mul3le  26038  coeeulem  26145  dgrcolem1  26195  dgrcolem2  26196  plycpn  26213  dvntaylp  26295  pserdv  26355  pige3ALT  26445  cxpcn2  26672  rlimcnp3  26893  lgamgulmlem2  26956  basellem2  27008  pntrsumo1  27492  pntrsumbnd  27493  nosupbnd1lem1  27636  noinfbnd1lem1  27651  cutlt  27863  nbupgr  29307  nbumgrvtx  29309  nbgr2vtx1edg  29313  cusgrexilem2  29405  ifpsnprss  29586  1pthon2ve  30116  suppovss  32637  offinsupp1  32683  xrsmulgzz  32976  gsummpt2co  33014  gsumfs2d  33021  gsumpart  33023  gsumhashmul  33027  symgcom2  33039  pmtrcnelor  33046  tocycfvres1  33065  tocycfvres2  33066  cycpmconjvlem  33096  elrgspnlem1  33192  elrgspnlem2  33193  elrgspnsubrunlem1  33197  fracf1  33256  idomsubr  33258  fldgenid  33268  lindfpropd  33329  lsmsnpridl  33345  qusrn  33356  elrspunidl  33375  ssdifidl  33404  mxidlprm  33417  ssmxidl  33421  rlmdim  33581  rgmoddimOLD  33582  tngdim  33585  matdim  33587  ply1degltdimlem  33594  fedgmullem1  33601  fldextrspunlsplem  33644  algextdeglem8  33690  constrmon  33710  mdetpmtr1  33789  zarclssn  33839  zart0  33845  zarcmplem  33847  pnfneige0  33917  pwsiga  34096  baselcarsg  34273  boolesineq  34422  efmul2picn  34563  reprfz1  34591  breprexplemc  34599  circlemeth  34607  circlevma  34609  circlemethhgt  34610  hgt750lemb  34623  hgt750lema  34624  hgt750leme  34625  tgoldbachgtde  34627  satfsschain  35336  mrsubff1  35486  mrsub0  35488  mrsubccat  35490  mrsubcn  35491  msubff1  35528  mthmpps  35554  wzel  35797  knoppndvlem6  36490  knoppndv  36507  bj-elpwg  37025  bj-restpw  37065  bj-restb  37067  bj-restuni2  37071  ftc1cnnclem  37670  ftc1cnnc  37671  ftc2nc  37681  areacirclem3  37689  welb  37715  cnresima  37743  rngoidl  38003  1psubclN  39923  cdlemefrs32fva  40379  lcmineqlem9  42010  lcmineqlem12  42013  intlewftc  42034  aks4d1p9  42061  primrootspoweq0  42079  sticksstones11  42129  aks6d1c6lem3  42145  aks6d1c6lem4  42146  aks6d1c6lem5  42150  aks6d1c7lem1  42153  addinvcom  42405  evlsvvvallem  42534  evlsvvvallem2  42535  evlsvvval  42536  selvcllem4  42554  selvvvval  42558  evlselv  42560  rgspnid  43141  oacl2g  43303  omabs2  43305  omcl2  43306  tfsconcatb0  43317  naddgeoa  43367  harval3  43511  cnvtrucl0  43597  brfvrtrcld  43707  clsk3nimkb  44013  k0004ss2  44125  extoimad  44137  mnuprd  44249  dvconstbi  44307  ssinc  45065  ssdec  45066  restopn3  45129  founiiun  45157  choicefi  45178  islptre  45601  fnlimfvre  45656  addccncf2  45858  fsumcncf  45860  cncfperiod  45861  negcncfg  45863  cncfuni  45868  icccncfext  45869  cncficcgt0  45870  fprodcncf  45882  dvcnre  45898  fperdvper  45901  itgsinexplem1  45936  itgcoscmulx  45951  smfpimne2  46822  predgclnbgrel  47823  isubgrvtxuhgr  47848  fldhmsubcALTV  48305  elbigolo1  48530  iunlub  48793  iinglb  48794  sepfsepc  48900