Theorem ssidd 4006

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  funfvima2d  7234  suppofss1d  8189  suppofss2d  8190  fpr1  8288  ralxpmap  8890  fissuni  9357  fsuppmptif  9394  fsuppco2  9398  fsuppcor  9399  mapfienlem1  9400  mapfienlem2  9401  cantnfp1lem1  9673  cantnfp1lem3  9675  cantnflem1  9684  htalem  9891  ackbij2lem4  10237  cflim2  10258  fin23lem15  10329  wunex2  10733  swrd0  14608  rtrclreclem1  15004  summolem3  15660  isum  15665  fsumser  15676  fsumcl  15679  flo1  15800  prodmolem3  15877  iprod  15882  iprodn0  15884  fprodss  15892  fprodcl  15896  fprodclf  15936  rpnnen2lem11  16167  eulerthlem2  16715  mremre  17548  catsubcat  17789  yon11  18217  yon12  18218  yon2  18219  yonpropd  18221  oppcyon  18222  yonffth  18237  submid  18691  mulgnncl  18969  mulgnn0cl  18970  mulgcl  18971  subgid  19008  snsymgefmndeq  19262  symggen  19338  gsumzcl2  19778  gsumzf1o  19780  gsum2dlem1  19838  gsum2dlem2  19839  gsum2d  19840  gsumxp2  19848  dprdfinv  19889  dmdprdsplitlem  19907  dprd2db  19913  dpjidcl  19928  ablfac1eu  19943  ablfaclem2  19956  gsumdixp  20131  primefld  20421  lcomfsupp  20512  lss1  20549  rlmbas  20817  rlmplusg  20818  rlm0  20819  rlmmulr  20821  rlmsca  20822  rlmsca2  20823  rlmvsca  20824  rlmtopn  20825  rlmds  20826  regsumsupp  21175  frlmsslsp  21351  frlmup1  21353  rnasclassa  21449  mplsubglem  21558  mpllsslem  21559  mplsubrglem  21563  mplcoe1  21592  mplcoe5  21595  mplbas2  21597  evlslem4  21637  psrbagev1  21638  psrbagev1OLD  21639  evlslem2  21642  mhpvscacl  21697  mamures  21892  cpmadumatpolylem2  22384  neiptopuni  22634  neiptoptop  22635  restopn2  22681  rncmp  22900  cmpfi  22912  conncn  22930  llyidm  22992  nllyidm  22993  toplly  22994  kgentopon  23042  kgencn2  23061  ptcld  23117  qtopuni  23206  supnfcls  23524  utopbas  23740  metustfbas  24066  rrxcph  24909  rrxmval  24922  rrxdstprj1  24926  evthicc2  24977  volcn  25123  dvres3  25430  dvres3a  25431  dvidlem  25432  dvmptresicc  25433  dvnadd  25446  dvnres  25448  dvaddbr  25455  dvmulbr  25456  dvcmul  25461  dvcmulf  25462  dvcobr  25463  dvcjbr  25466  dvrec  25472  dveflem  25496  dvef  25497  dvlipcn  25511  dvgt0lem2  25520  lhop1lem  25530  ftc1cn  25560  ftc2  25561  itgpowd  25567  deg1mul3le  25634  coeeulem  25738  dgrcolem1  25787  dgrcolem2  25788  plycpn  25802  dvntaylp  25883  pserdv  25941  pige3ALT  26029  cxpcn2  26254  rlimcnp3  26472  lgamgulmlem2  26534  basellem2  26586  pntrsumo1  27068  pntrsumbnd  27069  nosupbnd1lem1  27211  noinfbnd1lem1  27226  cutlt  27419  nbupgr  28601  nbumgrvtx  28603  nbgr2vtx1edg  28607  cusgrexilem2  28699  ifpsnprss  28880  1pthon2ve  29407  suppovss  31906  offinsupp1  31952  xrsmulgzz  32179  gsummpt2co  32200  gsumpart  32207  gsumhashmul  32208  symgcom2  32245  pmtrcnelor  32252  tocycfvres1  32269  tocycfvres2  32270  cycpmconjvlem  32300  fldgenid  32409  lindfpropd  32498  lsmsnpridl  32508  qusrn  32520  elrspunidl  32546  mxidlprm  32586  ssmxidl  32590  evls1fpws  32646  rlmdim  32694  rgmoddimOLD  32695  tngdim  32698  matdim  32700  ply1degltdimlem  32707  fedgmullem1  32714  mdetpmtr1  32803  zarclssn  32853  zart0  32859  zarcmplem  32861  pnfneige0  32931  pwsiga  33128  baselcarsg  33305  efmul2picn  33608  reprfz1  33636  breprexplemc  33644  circlemeth  33652  circlevma  33654  circlemethhgt  33655  hgt750lemb  33668  hgt750lema  33669  hgt750leme  33670  tgoldbachgtde  33672  satfsschain  34355  mrsubff1  34505  mrsub0  34507  mrsubccat  34509  mrsubcn  34510  msubff1  34547  mthmpps  34573  wzel  34796  gg-dvcnp2  35174  gg-dvmulbr  35175  gg-dvcobr  35176  knoppndvlem6  35393  knoppndv  35410  bj-elpwg  35933  bj-restpw  35973  bj-restb  35975  bj-restuni2  35979  ftc1cnnclem  36559  ftc1cnnc  36560  ftc2nc  36570  areacirclem3  36578  welb  36604  cnresima  36632  rngoidl  36892  1psubclN  38815  cdlemefrs32fva  39271  lcmineqlem9  40902  lcmineqlem12  40905  intlewftc  40926  aks4d1p9  40953  sticksstones11  40972  mhmcompl  41120  evlsvvvallem  41133  evlsvvvallem2  41134  evlsvvval  41135  selvcllem4  41153  selvvvval  41157  evlselv  41159  addinvcom  41304  rgspnid  41914  oacl2g  42080  omabs2  42082  omcl2  42083  tfsconcatb0  42094  naddgeoa  42145  harval3  42289  cnvtrucl0  42375  brfvrtrcld  42485  clsk3nimkb  42791  k0004ss2  42903  extoimad  42916  mnuprd  43035  dvconstbi  43093  ssinc  43776  ssdec  43777  restopn3  43845  founiiun  43875  choicefi  43899  islptre  44335  fnlimfvre  44390  addccncf2  44592  fsumcncf  44594  cncfperiod  44595  negcncfg  44597  cncfuni  44602  icccncfext  44603  cncficcgt0  44604  fprodcncf  44616  dvcnre  44632  fperdvper  44635  itgsinexplem1  44670  itgcoscmulx  44685  smfpimne2  45556  submgmid  46563  subrngid  46728  rng2idl1cntr  46790  rnghmsscmap2  46871  rhmsscmap2  46917  fldhmsubc  46982  fldhmsubcALTV  47000  elbigolo1  47243  sepfsepc  47560