Theorem ssidd 4032

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3976

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

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

This theorem is referenced by:  funfvima2d  7269  suppofss1d  8245  suppofss2d  8246  fpr1  8344  ralxpmap  8954  fissuni  9427  fsuppssov1  9453  fsuppmptif  9468  fsuppco2  9472  fsuppcor  9473  mapfienlem1  9474  mapfienlem2  9475  cantnfp1lem1  9747  cantnfp1lem3  9749  cantnflem1  9758  htalem  9965  ackbij2lem4  10310  cflim2  10332  fin23lem15  10403  wunex2  10807  swrd0  14706  rtrclreclem1  15106  summolem3  15762  isum  15767  fsumser  15778  fsumcl  15781  flo1  15902  prodmolem3  15981  iprod  15986  iprodn0  15988  fprodss  15996  fprodcl  16000  fprodclf  16040  rpnnen2lem11  16272  eulerthlem2  16829  mremre  17662  catsubcat  17903  yon11  18334  yon12  18335  yon2  18336  yonpropd  18338  oppcyon  18339  yonffth  18354  submgmid  18744  submid  18845  mulgnncl  19129  mulgnn0cl  19130  mulgcl  19131  subgid  19168  snsymgefmndeq  19436  symggen  19512  gsumzcl2  19952  gsumzf1o  19954  gsum2dlem1  20012  gsum2dlem2  20013  gsum2d  20014  gsumxp2  20022  dprdfinv  20063  dmdprdsplitlem  20081  dprd2db  20087  dpjidcl  20102  ablfac1eu  20117  ablfaclem2  20130  gsumdixp  20342  subrngid  20575  rnghmsscmap2  20651  rhmsscmap2  20680  fldhmsubc  20808  primefld  20828  lcomfsupp  20922  lss1  20959  rlmbas  21223  rlmplusg  21224  rlm0  21225  rlmmulr  21227  rlmsca  21228  rlmsca2  21229  rlmvsca  21230  rlmtopn  21231  rlmds  21232  rng2idl1cntr  21338  regsumsupp  21663  frlmsslsp  21839  frlmup1  21841  rnasclassa  21938  mplsubglem  22042  mpllsslem  22043  mplsubrglem  22047  mplcoe1  22078  mplcoe5  22081  mplbas2  22083  evlslem4  22123  psrbagev1  22124  evlslem2  22126  mhpvscacl  22181  psdmplcl  22189  evls1fpws  22394  evl1maprhm  22404  mhmcompl  22405  mamures  22422  cpmadumatpolylem2  22909  neiptopuni  23159  neiptoptop  23160  restopn2  23206  rncmp  23425  cmpfi  23437  conncn  23455  llyidm  23517  nllyidm  23518  toplly  23519  kgentopon  23567  kgencn2  23586  ptcld  23642  qtopuni  23731  supnfcls  24049  utopbas  24265  metustfbas  24591  rrxcph  25445  rrxmval  25458  rrxdstprj1  25462  evthicc2  25514  volcn  25660  dvres3  25968  dvres3a  25969  dvidlem  25970  dvmptresicc  25971  dvcnp2  25975  dvnadd  25985  dvnres  25987  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcmul  26001  dvcmulf  26002  dvcobr  26003  dvcobrOLD  26004  dvcjbr  26007  dvrec  26013  dveflem  26037  dvef  26038  dvlipcn  26053  dvgt0lem2  26062  lhop1lem  26072  ftc1cn  26104  ftc2  26105  itgpowd  26111  deg1mul3le  26176  coeeulem  26283  dgrcolem1  26333  dgrcolem2  26334  plycpn  26349  dvntaylp  26431  pserdv  26491  pige3ALT  26580  cxpcn2  26807  rlimcnp3  27028  lgamgulmlem2  27091  basellem2  27143  pntrsumo1  27627  pntrsumbnd  27628  nosupbnd1lem1  27771  noinfbnd1lem1  27786  cutlt  27984  nbupgr  29379  nbumgrvtx  29381  nbgr2vtx1edg  29385  cusgrexilem2  29477  ifpsnprss  29659  1pthon2ve  30186  suppovss  32697  offinsupp1  32741  xrsmulgzz  32992  gsummpt2co  33031  gsumpart  33038  gsumhashmul  33040  symgcom2  33077  pmtrcnelor  33084  tocycfvres1  33103  tocycfvres2  33104  cycpmconjvlem  33134  fracf1  33274  idomsubr  33276  fldgenid  33286  lindfpropd  33375  lsmsnpridl  33391  qusrn  33402  elrspunidl  33421  ssdifidl  33450  mxidlprm  33463  ssmxidl  33467  rlmdim  33622  rgmoddimOLD  33623  tngdim  33626  matdim  33628  ply1degltdimlem  33635  fedgmullem1  33642  algextdeglem8  33715  constrmon  33734  mdetpmtr1  33769  zarclssn  33819  zart0  33825  zarcmplem  33827  pnfneige0  33897  pwsiga  34094  baselcarsg  34271  efmul2picn  34573  reprfz1  34601  breprexplemc  34609  circlemeth  34617  circlevma  34619  circlemethhgt  34620  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  tgoldbachgtde  34637  satfsschain  35332  mrsubff1  35482  mrsub0  35484  mrsubccat  35486  mrsubcn  35487  msubff1  35524  mthmpps  35550  wzel  35788  knoppndvlem6  36483  knoppndv  36500  bj-elpwg  37018  bj-restpw  37058  bj-restb  37060  bj-restuni2  37064  ftc1cnnclem  37651  ftc1cnnc  37652  ftc2nc  37662  areacirclem3  37670  welb  37696  cnresima  37724  rngoidl  37984  1psubclN  39901  cdlemefrs32fva  40357  lcmineqlem9  41994  lcmineqlem12  41997  intlewftc  42018  aks4d1p9  42045  primrootspoweq0  42063  sticksstones11  42113  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6lem5  42134  aks6d1c7lem1  42137  addinvcom  42407  evlsvvvallem  42516  evlsvvvallem2  42517  evlsvvval  42518  selvcllem4  42536  selvvvval  42540  evlselv  42542  rgspnid  43129  oacl2g  43292  omabs2  43294  omcl2  43295  tfsconcatb0  43306  naddgeoa  43356  harval3  43500  cnvtrucl0  43586  brfvrtrcld  43696  clsk3nimkb  44002  k0004ss2  44114  extoimad  44126  mnuprd  44245  dvconstbi  44303  ssinc  44989  ssdec  44990  restopn3  45056  founiiun  45086  choicefi  45107  islptre  45540  fnlimfvre  45595  addccncf2  45797  fsumcncf  45799  cncfperiod  45800  negcncfg  45802  cncfuni  45807  icccncfext  45808  cncficcgt0  45809  fprodcncf  45821  dvcnre  45837  fperdvper  45840  itgsinexplem1  45875  itgcoscmulx  45890  smfpimne2  46761  predgclnbgrel  47711  isubgrvtxuhgr  47736  fldhmsubcALTV  48056  elbigolo1  48291  sepfsepc  48607