Theorem ssidd 3946

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3890

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

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

This theorem is referenced by:  funfvima2d  7178  suppofss1d  8145  suppofss2d  8146  fpr1  8244  ralxpmap  8835  fissuni  9258  fsuppssov1  9288  fsuppmptif  9303  fsuppco2  9307  fsuppcor  9308  mapfienlem1  9309  mapfienlem2  9310  cantnfp1lem1  9588  cantnfp1lem3  9590  cantnflem1  9599  htalem  9809  ackbij2lem4  10152  cflim2  10174  fin23lem15  10245  wunex2  10650  swrd0  14610  rtrclreclem1  15008  summolem3  15665  isum  15670  fsumser  15681  fsumcl  15684  flo1  15808  prodmolem3  15887  iprod  15892  iprodn0  15894  fprodss  15902  fprodcl  15906  fprodclf  15946  rpnnen2lem11  16180  eulerthlem2  16741  mremre  17555  catsubcat  17795  yon11  18219  yon12  18220  yon2  18221  yonpropd  18223  oppcyon  18224  yonffth  18239  submgmid  18663  submid  18767  mulgnncl  19054  mulgnn0cl  19055  mulgcl  19056  subgid  19093  snsymgefmndeq  19359  symggen  19434  gsumzcl2  19874  gsumzf1o  19876  gsum2dlem1  19934  gsum2dlem2  19935  gsum2d  19936  gsumxp2  19944  dprdfinv  19985  dmdprdsplitlem  20003  dprd2db  20009  dpjidcl  20024  ablfac1eu  20039  ablfaclem2  20052  gsumdixp  20287  subrngid  20515  rnghmsscmap2  20595  rhmsscmap2  20624  fldhmsubc  20751  primefld  20771  lcomfsupp  20886  lss1  20922  rlmbas  21178  rlmplusg  21179  rlm0  21180  rlmmulr  21182  rlmsca  21183  rlmsca2  21184  rlmvsca  21185  rlmtopn  21186  rlmds  21187  rng2idl1cntr  21293  regsumsupp  21610  frlmsslsp  21784  frlmup1  21786  rnasclassa  21883  mplsubglem  21986  mpllsslem  21987  mplsubrglem  21991  mplcoe1  22024  mplcoe5  22027  mplbas2  22029  evlslem4  22063  psrbagev1  22064  evlslem2  22066  evlsvvvallem  22078  evlsvvvallem2  22079  evlsvvval  22080  mhpvscacl  22129  psdmplcl  22137  evls1fpws  22343  evl1maprhm  22353  mhmcompl  22354  mamures  22371  cpmadumatpolylem2  22856  neiptopuni  23104  neiptoptop  23105  restopn2  23151  rncmp  23370  cmpfi  23382  conncn  23400  llyidm  23462  nllyidm  23463  toplly  23464  kgentopon  23512  kgencn2  23531  ptcld  23587  qtopuni  23676  supnfcls  23994  utopbas  24209  metustfbas  24531  rrxcph  25368  rrxmval  25381  rrxdstprj1  25385  evthicc2  25436  volcn  25582  dvres3  25889  dvres3a  25890  dvidlem  25891  dvmptresicc  25892  dvcnp2  25896  dvnadd  25905  dvnres  25907  dvaddbr  25914  dvmulbr  25915  dvcmul  25920  dvcmulf  25921  dvcobr  25922  dvcjbr  25925  dvrec  25931  dveflem  25955  dvef  25956  dvlipcn  25971  dvgt0lem2  25980  lhop1lem  25990  ftc1cn  26022  ftc2  26023  itgpowd  26029  deg1mul3le  26094  coeeulem  26201  dgrcolem1  26250  dgrcolem2  26251  plycpn  26268  dvntaylp  26350  pserdv  26410  pige3ALT  26500  cxpcn2  26727  rlimcnp3  26948  lgamgulmlem2  27011  basellem2  27063  pntrsumo1  27547  pntrsumbnd  27548  nosupbnd1lem1  27691  noinfbnd1lem1  27706  cutlt  27943  nbupgr  29432  nbumgrvtx  29434  nbgr2vtx1edg  29438  cusgrexilem2  29530  ifpsnprss  29711  1pthon2ve  30244  suppovss  32774  offinsupp1  32819  xrsmulgzz  33089  gsummpt2co  33129  gsummptrev  33137  gsummptp1  33138  gsumfs2d  33142  gsumpart  33144  gsumhashmul  33148  gsummulsubdishift1  33149  symgcom2  33165  pmtrcnelor  33172  tocycfvres1  33191  tocycfvres2  33192  cycpmconjvlem  33222  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnsubrunlem1  33328  fracf1  33388  idomsubr  33390  fldgenid  33400  lindfpropd  33462  lsmsnpridl  33478  qusrn  33489  elrspunidl  33508  ssdifidl  33537  mxidlprm  33550  ssmxidl  33554  evlextv  33706  mplvrpmrhm  33711  vieta  33744  srapwov  33753  rlmdim  33774  rgmoddimOLD  33775  tngdim  33778  matdim  33780  ply1degltdimlem  33787  fedgmullem1  33794  fldextrspunlsplem  33838  algextdeglem8  33889  constrmon  33909  mdetpmtr1  33988  zarclssn  34038  zart0  34044  zarcmplem  34046  pnfneige0  34116  pwsiga  34295  baselcarsg  34471  boolesineq  34620  efmul2picn  34761  reprfz1  34789  breprexplemc  34797  circlemeth  34805  circlevma  34807  circlemethhgt  34808  hgt750lemb  34821  hgt750lema  34822  hgt750leme  34823  tgoldbachgtde  34825  satfsschain  35567  mrsubff1  35717  mrsub0  35719  mrsubccat  35721  mrsubcn  35722  msubff1  35759  mthmpps  35785  wzel  36025  knoppndvlem6  36790  knoppndv  36807  bj-elpwg  37372  bj-restpw  37417  bj-restb  37419  bj-restuni2  37423  ftc1cnnclem  38023  ftc1cnnc  38024  ftc2nc  38034  areacirclem3  38042  welb  38068  cnresima  38096  rngoidl  38356  1psubclN  40401  cdlemefrs32fva  40857  lcmineqlem9  42487  lcmineqlem12  42490  intlewftc  42511  aks4d1p9  42538  primrootspoweq0  42556  sticksstones11  42606  aks6d1c6lem3  42622  aks6d1c6lem4  42623  aks6d1c6lem5  42627  aks6d1c7lem1  42630  addinvcom  42875  selvcllem4  43025  selvvvval  43029  evlselv  43031  rgspnid  43611  oacl2g  43773  omabs2  43775  omcl2  43776  tfsconcatb0  43787  naddgeoa  43837  harval3  43980  cnvtrucl0  44066  brfvrtrcld  44176  clsk3nimkb  44482  k0004ss2  44594  extoimad  44606  mnuprd  44718  dvconstbi  44776  ssinc  45532  ssdec  45533  restopn3  45596  founiiun  45624  choicefi  45644  islptre  46064  fnlimfvre  46117  addccncf2  46319  fsumcncf  46321  cncfperiod  46322  negcncfg  46324  cncfuni  46329  icccncfext  46330  cncficcgt0  46331  fprodcncf  46343  dvcnre  46359  fperdvper  46362  itgsinexplem1  46397  itgcoscmulx  46412  smfpimne2  47283  predgclnbgrel  48312  isubgrvtxuhgr  48337  fldhmsubcALTV  48806  elbigolo1  49030  iunlub  49293  iinglb  49294  sepfsepc  49400