Theorem ssidd 4003

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  funfvima2d  7244  suppofss1d  8210  suppofss2d  8211  fpr1  8309  ralxpmap  8915  fissuni  9382  fsuppssov1  9408  fsuppmptif  9423  fsuppco2  9427  fsuppcor  9428  mapfienlem1  9429  mapfienlem2  9430  cantnfp1lem1  9702  cantnfp1lem3  9704  cantnflem1  9713  htalem  9920  ackbij2lem4  10266  cflim2  10287  fin23lem15  10358  wunex2  10762  swrd0  14641  rtrclreclem1  15037  summolem3  15693  isum  15698  fsumser  15709  fsumcl  15712  flo1  15833  prodmolem3  15910  iprod  15915  iprodn0  15917  fprodss  15925  fprodcl  15929  fprodclf  15969  rpnnen2lem11  16201  eulerthlem2  16751  mremre  17584  catsubcat  17825  yon11  18256  yon12  18257  yon2  18258  yonpropd  18260  oppcyon  18261  yonffth  18276  submgmid  18666  submid  18762  mulgnncl  19044  mulgnn0cl  19045  mulgcl  19046  subgid  19083  snsymgefmndeq  19349  symggen  19425  gsumzcl2  19865  gsumzf1o  19867  gsum2dlem1  19925  gsum2dlem2  19926  gsum2d  19927  gsumxp2  19935  dprdfinv  19976  dmdprdsplitlem  19994  dprd2db  20000  dpjidcl  20015  ablfac1eu  20030  ablfaclem2  20043  gsumdixp  20255  subrngid  20486  rnghmsscmap2  20562  rhmsscmap2  20591  fldhmsubc  20673  primefld  20693  lcomfsupp  20785  lss1  20822  rlmbas  21086  rlmplusg  21087  rlm0  21088  rlmmulr  21090  rlmsca  21091  rlmsca2  21092  rlmvsca  21093  rlmtopn  21094  rlmds  21095  rng2idl1cntr  21195  regsumsupp  21554  frlmsslsp  21730  frlmup1  21732  rnasclassa  21828  mplsubglem  21941  mpllsslem  21942  mplsubrglem  21946  mplcoe1  21975  mplcoe5  21978  mplbas2  21980  evlslem4  22020  psrbagev1  22021  psrbagev1OLD  22022  evlslem2  22025  mhpvscacl  22078  psdmplcl  22086  evls1fpws  22288  mamures  22305  cpmadumatpolylem2  22797  neiptopuni  23047  neiptoptop  23048  restopn2  23094  rncmp  23313  cmpfi  23325  conncn  23343  llyidm  23405  nllyidm  23406  toplly  23407  kgentopon  23455  kgencn2  23474  ptcld  23530  qtopuni  23619  supnfcls  23937  utopbas  24153  metustfbas  24479  rrxcph  25333  rrxmval  25346  rrxdstprj1  25350  evthicc2  25402  volcn  25548  dvres3  25855  dvres3a  25856  dvidlem  25857  dvmptresicc  25858  dvcnp2  25862  dvnadd  25872  dvnres  25874  dvaddbr  25881  dvmulbr  25882  dvmulbrOLD  25883  dvcmul  25888  dvcmulf  25889  dvcobr  25890  dvcobrOLD  25891  dvcjbr  25894  dvrec  25900  dveflem  25924  dvef  25925  dvlipcn  25940  dvgt0lem2  25949  lhop1lem  25959  ftc1cn  25991  ftc2  25992  itgpowd  25998  deg1mul3le  26065  coeeulem  26171  dgrcolem1  26221  dgrcolem2  26222  plycpn  26237  dvntaylp  26319  pserdv  26379  pige3ALT  26467  cxpcn2  26694  rlimcnp3  26912  lgamgulmlem2  26975  basellem2  27027  pntrsumo1  27511  pntrsumbnd  27512  nosupbnd1lem1  27654  noinfbnd1lem1  27669  cutlt  27865  nbupgr  29170  nbumgrvtx  29172  nbgr2vtx1edg  29176  cusgrexilem2  29268  ifpsnprss  29450  1pthon2ve  29977  suppovss  32478  offinsupp1  32522  xrsmulgzz  32749  gsummpt2co  32775  gsumpart  32782  gsumhashmul  32783  symgcom2  32820  pmtrcnelor  32827  tocycfvres1  32844  tocycfvres2  32845  cycpmconjvlem  32875  fracf1  33006  idomsubr  33008  fldgenid  33019  lindfpropd  33110  lsmsnpridl  33120  qusrn  33132  elrspunidl  33157  mxidlprm  33196  ssmxidl  33200  rlmdim  33307  rgmoddimOLD  33308  tngdim  33311  matdim  33313  ply1degltdimlem  33320  fedgmullem1  33327  algextdeglem8  33392  mdetpmtr1  33424  zarclssn  33474  zart0  33480  zarcmplem  33482  pnfneige0  33552  pwsiga  33749  baselcarsg  33926  efmul2picn  34228  reprfz1  34256  breprexplemc  34264  circlemeth  34272  circlevma  34274  circlemethhgt  34275  hgt750lemb  34288  hgt750lema  34289  hgt750leme  34290  tgoldbachgtde  34292  satfsschain  34974  mrsubff1  35124  mrsub0  35126  mrsubccat  35128  mrsubcn  35129  msubff1  35166  mthmpps  35192  wzel  35420  knoppndvlem6  35992  knoppndv  36009  bj-elpwg  36531  bj-restpw  36571  bj-restb  36573  bj-restuni2  36577  ftc1cnnclem  37164  ftc1cnnc  37165  ftc2nc  37175  areacirclem3  37183  welb  37209  cnresima  37237  rngoidl  37497  1psubclN  39417  cdlemefrs32fva  39873  lcmineqlem9  41508  lcmineqlem12  41511  intlewftc  41532  aks4d1p9  41559  primrootspoweq0  41577  sticksstones11  41628  aks6d1c6lem3  41644  aks6d1c6lem4  41645  aks6d1c6lem5  41649  aks6d1c7lem1  41652  mhmcompl  41781  evlsvvvallem  41794  evlsvvvallem2  41795  evlsvvval  41796  selvcllem4  41814  selvvvval  41818  evlselv  41820  addinvcom  41986  rgspnid  42596  oacl2g  42759  omabs2  42761  omcl2  42762  tfsconcatb0  42773  naddgeoa  42824  harval3  42968  cnvtrucl0  43054  brfvrtrcld  43164  clsk3nimkb  43470  k0004ss2  43582  extoimad  43594  mnuprd  43713  dvconstbi  43771  ssinc  44453  ssdec  44454  restopn3  44522  founiiun  44552  choicefi  44573  islptre  45007  fnlimfvre  45062  addccncf2  45264  fsumcncf  45266  cncfperiod  45267  negcncfg  45269  cncfuni  45274  icccncfext  45275  cncficcgt0  45276  fprodcncf  45288  dvcnre  45304  fperdvper  45307  itgsinexplem1  45342  itgcoscmulx  45357  smfpimne2  46228  fldhmsubcALTV  47395  elbigolo1  47630  sepfsepc  47946