Theorem ssidd 3931

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827

This proof depends on definitions:  df-bi 210  df-ss 3896

This theorem is used by:  pwidg  4576  funfvima2d  7238  suppofss1d  8222  suppofss2d  8223  fpr1  8322  ralxpmap  8925  fissuni  9347  fsuppssov1  9377  fsuppmptif  9392  fsuppco2  9396  fsuppcor  9397  mapfienlem1  9398  mapfienlem2  9399  cantnfp1lem1  9680  cantnfp1lem3  9682  cantnflem1  9691  htalem  9962  ackbij2lem4  10320  cflim2  10342  fin23lem15  10413  wunex2  10824  swrd0  14809  rtrclreclem1  15211  summolem3  15881  isum  15886  fsumser  15897  fsumcl  15900  flo1  16024  prodmolem3  16101  iprod  16106  iprodn0  16108  fprodss  16116  fprodcl  16120  fprodclf  16160  rpnnen2lem11  16393  eulerthlem2  16960  mremre  17775  catsubcat  18015  yon11  18439  yon12  18440  yon2  18441  yonpropd  18443  oppcyon  18444  yonffth  18459  submgmid  18896  submid  19006  mulgnncl  19300  mulgnn0cl  19301  mulgcl  19302  subgid  19339  snsymgefmndeq  19610  symggen  19685  gsumzcl2  20125  gsumzf1o  20127  gsum2dlem1  20185  gsum2dlem2  20186  gsum2d  20187  gsumxp2  20195  dprdfinv  20236  dmdprdsplitlem  20254  dprd2db  20260  dpjidcl  20275  ablfac1eu  20290  ablfaclem2  20303  gsumdixp  20549  subrngid  20802  rnghmsscmap2  20882  rhmsscmap2  20911  fldhmsubc  21043  primefld  21063  lcomfsupp  21178  lss1  21214  rlmbas  21469  rlmplusg  21470  rlm0  21471  rlmmulr  21473  rlmsca  21474  rlmsca2  21475  rlmvsca  21476  rlmtopn  21477  rlmds  21478  rng2idl1cntr  21602  ssdifidl  21642  regsumsupp  21929  frlmsslsp  22103  frlmup1  22105  rnasclassa  22204  mplsubglem  22307  mpllsslem  22308  mplsubrglem  22312  mplcoe1  22347  mplcoe5  22350  mplbas2  22352  evlslem4  22386  psrbagev1  22387  evlslem2  22389  evlsvvvallem  22401  evlsvvvallem2  22402  evlsvvval  22403  mhmcompl  22431  selvcllem4  22448  selvvvval  22452  mhpvscacl  22476  psdmplcl  22484  evls1fpws  22688  evl1maprhm  22698  mamures  22713  cpmadumatpolylem2  23201  neiptopuni  23449  neiptoptop  23450  restopn2  23496  rncmp  23715  cmpfi  23727  conncn  23745  llyidm  23808  nllyidm  23809  toplly  23810  kgentopon  23858  kgencn2  23877  ptcld  23933  qtopuni  24022  supnfcls  24340  utopbas  24555  metustfbas  24877  rrxcph  25714  rrxmval  25727  rrxdstprj1  25731  evthicc2  25782  volcn  25928  dvres3  26234  dvres3a  26235  dvidlem  26236  dvmptresicc  26237  dvcnp2  26241  dvnadd  26250  dvnres  26252  dvaddbr  26259  dvmulbr  26260  dvcmul  26265  dvcmulf  26266  dvcobr  26267  dvcjbr  26270  dvrec  26276  dveflem  26300  dvef  26301  dvlipcn  26315  dvgt0lem2  26324  lhop1lem  26334  ftc1cn  26364  ftc2  26365  itgpowd  26371  deg1mul3le  26436  coeeulem  26544  dgrcolem1  26593  dgrcolem2  26594  plycpn  26611  rnplynfin  26631  dvntaylp  26699  pserdv  26757  pige3ALT  26849  cxpcn2  27075  rlimcnp3  27296  lgamgulmlem2  27358  basellem2  27410  pntrsumo1  27893  pntrsumbnd  27894  nosupbnd1lem1  28066  noinfbnd1lem1  28081  cutlt  28319  nbupgr  29926  nbumgrvtx  29928  nbgr2vtx1edg  29932  cusgrexilem2  30024  ifpsnprss  30204  1pthon2ve  30756  suppovss  33317  offinsupp1  33361  xrsmulgzz  33613  gsummpt2co  33652  gsummptrev  33660  gsummptp1  33661  gsumfs2d  33665  gsumpart  33667  gsumhashmul  33671  gsummulsubdishift1  33672  symgcom2  33688  pmtrcnelor  33695  tocycfvres1  33714  tocycfvres2  33715  cycpmconjvlem  33745  elrgspnlem1  33846  elrgspnlem2  33847  elrgspnsubrunlem1  33851  fracf1  33912  idomsubr  33914  fldgenid  33924  lindfpropd  33980  lsmsnpridl  33994  qusrn  34003  elrspunidl  34021  mxidlprm  34038  ssmxidl  34042  selvply1rhmlemb  34194  evlextv  34217  mplvrpmrhm  34222  vieta  34255  srapwov  34264  rlmdim  34285  tngdim  34288  matdim  34290  ply1degltdimlem  34297  fedgmullem1  34304  fldextrspunlsplem  34348  algextdeglem8  34399  constrmon  34419  mdetpmtr1  34498  zarclssn  34548  zart0  34554  zarcmplem  34556  pnfneige0  34626  pwsiga  34805  baselcarsg  34981  boolesineq  35130  efmul2picn  35268  reprfz1  35296  breprexplemc  35304  circlemeth  35312  circlevma  35314  circlemethhgt  35315  hgt750lemb  35328  hgt750lema  35329  hgt750leme  35330  tgoldbachgtde  35332  satfsschain  36198  mrsubff1  36348  mrsub0  36350  mrsubccat  36352  mrsubcn  36353  msubff1  36390  mthmpps  36416  wzel  36661  nmulprop  37014  knoppndvlem6  37458  knoppndv  37475  bj-elpwg  38042  bj-restpw  38088  bj-restb  38090  bj-restuni2  38094  ftc1cnnclem  38685  ftc1cnnc  38686  ftc2nc  38696  areacirclem3  38704  welb  38746  cnresima  38774  rngoidl  39034  1psubclN  41077  cdlemefrs32fva  41533  lcmineqlem9  43163  lcmineqlem12  43166  intlewftc  43187  aks4d1p9  43214  primrootspoweq0  43232  sticksstones11  43282  aks6d1c6lem3  43298  aks6d1c6lem4  43299  aks6d1c6lem5  43303  aks6d1c7lem1  43306  addinvcom  43559  evlselv  43693  rgspnid  44246  oacl2g  44408  omabs2  44410  omcl2  44411  tfsconcatb0  44422  naddgeoa  44472  harval3  44615  cnvtrucl0  44700  brfvrtrcld  44810  clsk3nimkb  45116  k0004ss2  45228  extoimad  45240  mnuprd  45336  dvconstbi  45394  ssinc  46178  ssdec  46179  restopn3  46242  founiiun  46270  choicefi  46290  islptre  46707  fnlimfvre  46760  addccncf2  46962  fsumcncf  46964  cncfperiod  46965  negcncfg  46967  cncfuni  46972  icccncfext  46973  cncficcgt0  46974  fprodcncf  46986  dvcnre  47002  fperdvper  47005  itgsinexplem1  47040  itgcoscmulx  47055  fourierdlem113  47305  smfpimne2  47926  predgclnbgrel  49013  isubgrvtxuhgr  49038  fldhmsubcALTV  49506  elbigolo1  49745  iunlub  50007  iinglb  50008  sepfsepc  50112