Theorem ssun1 4172

Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ssun1	⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Proof of Theorem ssun1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		orc 864	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 4148	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 233	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3986	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 844   ∈ wcel 2105   ∪ cun 3946   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  ssun2  4173  ssun3  4174  elun1  4176  difsssymdif  4252  inabs  4255  reuun1  4317  un00  4442  pwunss  4620  pwundif  4626  snsspr1  4817  snsstp1  4819  snsstp2  4820  uniintsn  4991  sofld  6186  sssucid  6444  fvrn0  6921  ovima0  7590  unexb  7739  dmexg  7898  xpord2indlem  8138  xpord3inddlem  8145  suppun  8174  dftpos2  8234  tpostpos2  8238  frrlem12  8288  frrlem13  8289  wfrlem14OLD  8328  wfrlem15OLD  8329  tfrlem11  8394  oaabs2  8654  ralxpmap  8896  domss2  9142  mapunen  9152  ac6sfi  9293  frfi  9294  unfir  9320  domunfican  9326  iunfi  9346  elfiun  9431  dffi3  9432  unwdomg  9585  unxpwdom2  9589  unxpwdom  9590  cantnfp1lem1  9679  cantnfp1lem3  9681  tc2  9743  unwf  9811  rankunb  9851  r0weon  10013  infxpenlem  10014  dfac2b  10131  djudoml  10185  cdainflem  10188  infunabs  10208  infdju  10209  infdif  10210  ackbij1lem15  10235  cfsmolem  10271  isfin4p1  10316  fin23lem11  10318  fin1a2lem10  10410  fin1a2lem13  10413  axdc3lem4  10454  axcclem  10458  zornn0g  10506  ttukeylem1  10510  ttukeylem5  10514  ttukeylem7  10516  fingch  10624  fpwwe2lem12  10643  gchac  10682  wunfi  10722  wundm  10729  wunex2  10739  inar1  10776  ressxr  11265  nnssnn0  12482  un0addcl  12512  un0mulcl  12513  nn0ssxnn0  12554  hashbclem  14418  hashf1lem1  14422  hashf1lem1OLD  14423  hashf1lem2  14424  ccatrn  14546  trclublem  14949  relexpdmg  14996  relexpaddg  15007  fsumsplit  15694  fsum2d  15724  fsumabs  15754  fsumrlim  15764  fsumo1  15765  incexclem  15789  fprodsplit  15917  fprod2d  15932  lcmfunsnlem1  16581  coprmprod  16605  vdwapid1  16915  vdwlem6  16926  ramcl2  16956  isstruct2  17089  srngbase  17262  srngplusg  17263  srngmulr  17264  lmodbase  17278  lmodplusg  17279  lmodsca  17280  ipsbase  17289  ipsaddg  17290  ipsmulr  17291  phlbase  17299  phlplusg  17300  phlsca  17301  odrngbas  17356  odrngplusg  17357  odrngmulr  17358  prdssca  17409  prdsbas  17410  prdsplusg  17411  prdsmulr  17412  prdsvsca  17413  prdsip  17414  prdsle  17415  prdsds  17417  prdstset  17419  imasbas  17465  imasplusg  17470  imasmulr  17471  imassca  17472  imasvsca  17473  imasip  17474  mreexexlem2d  17596  drsdirfi  18268  ipobas  18494  ipotset  18496  acsfiindd  18516  psdmrn  18536  dirdm  18563  grpinvfval  18906  mulgfval  18995  gsumzsplit  19843  gsumsplit2  19845  gsumzunsnd  19872  gsum2dlem2  19887  dprdfadd  19938  dmdprdsplit2lem  19963  dmdprdsplit2  19964  dmdprdsplit  19965  dprdsplit  19966  ablfac1eulem  19990  lspun  20830  lspsolv  20989  lsppratlem3  20995  islbs3  21001  lbsextlem2  21005  lbsextlem4  21007  cnfldbas  21236  cnfldadd  21237  cnfldmul  21238  cnfldcj  21239  cnfldtset  21240  cnfldle  21241  cnfldds  21242  psrbagaddclOLD  21791  psrbas  21806  psrplusg  21809  psrmulr  21813  mplsubglem  21868  mplcoe1  21902  mplcoe5  21905  mdetunilem9  22441  basdif0  22775  ordtbas2  23014  ordtbas  23015  ordtopn1  23017  leordtval2  23035  iocpnfordt  23038  icomnfordt  23039  uncmp  23226  fiuncmp  23227  bwth  23233  locfincmp  23349  comppfsc  23355  1stckgenlem  23376  1stckgen  23377  ptbasin  23400  ptbasfi  23404  dfac14lem  23440  dfac14  23441  ptuncnv  23630  ptunhmeo  23631  ptcmpfi  23636  fbun  23663  trfil2  23710  ufprim  23732  ufileu  23742  filufint  23743  ufildr  23754  fmfnfm  23781  hausflim  23804  fclsfnflim  23850  alexsubALTlem4  23873  tmdgsum  23918  tsmsgsum  23962  tsmsres  23967  tsmssplit  23975  tsmsxplem1  23976  ustssco  24038  ustuqtop1  24065  prdsxmetlem  24193  prdsbl  24319  icccmplem2  24658  fsumcn  24707  cnmpopc  24768  rrxmetlem  25254  rrxmet  25255  rrxdstprj1  25256  ovolctb2  25340  ovolunnul  25348  ovolfiniun  25349  nulmbl2  25384  finiunmbl  25392  volfiniun  25395  icombl  25412  ioombl  25413  uniiccdif  25426  mbfres2  25493  itg2splitlem  25597  itg2split  25598  itgfsum  25675  itgsplit  25684  itgsplitioo  25686  dvreslem  25757  dvaddbr  25787  dvmulbr  25788  dvmulbrOLD  25789  dvmptfsum  25826  lhop  25868  dvcnvrelem2  25870  mdegcl  25924  elplyr  26052  plyrem  26156  xrlimcnp  26813  fsumharmonic  26856  chtdif  27002  lgsdir2lem3  27172  lgsquadlem2  27226  dchrisum0lem1b  27360  pntrlog2bndlem6  27428  pntlemf  27450  nosupinfsep  27577  noetalem1  27586  scutun12  27655  cofcutrtime  27759  addsuniflem  27830  negsval  27850  mulsproplem12  27939  mulsproplem13  27940  mulsproplem14  27941  mulsuniflem  27961  mulsass  27978  precsexlem6  28022  precsexlem7  28023  precsexlem10  28026  precsexlem11  28027  ex-ss  30112  shsleji  31055  shsval2i  31072  ssjo  31132  sshhococi  31231  padct  32376  gsumle  32677  symgcom  32679  cycpmco2lem5  32724  cycpmco2lem6  32725  cycpmco2lem7  32726  cycpmco2  32727  gsumvsca1  32806  gsumvsca2  32807  elrspunsn  32986  mxidlprm  33025  idlsrgbas  33057  idlsrgplusg  33058  idlsrgmulr  33060  esumsplit  33514  esumpad2  33517  aean  33705  sxbrsigalem2  33748  bnj931  34244  subfacp1lem2b  34635  subfacp1lem3  34636  subfacp1lem5  34638  kur14lem7  34666  kur14lem9  34668  cvmliftlem10  34748  satfsschain  34818  fmlasssuc  34843  gg-cnfldbas  35635  mpocnfldadd  35636  mpocnfldmul  35637  gg-cnfldcj  35638  gg-cnfldtset  35639  gg-cnfldle  35640  gg-cnfldds  35641  refssfne  35706  filnetlem3  35728  bj-unrab  36269  bj-snglsstag  36325  bj-2upln0  36367  bj-ccssccbar  36561  rdgssun  36722  finixpnum  36936  matunitlindflem1  36947  mbfresfi  36997  prdsbnd  37124  heibor1lem  37140  rrnequiv  37166  paddunssN  39142  sspadd1  39149  sspadd2  39150  pclfinN  39234  dochdmj1  40724  dvhdimlem  40778  elrfi  41894  mzpcompact2lem  41951  eldioph2  41962  eldioph4b  42011  ttac  42237  pwssplit4  42293  pwslnmlem2  42297  isnumbasgrplem2  42308  algbase  42382  algaddg  42383  algmulr  42384  fiuneneq  42401  idomsubgmo  42402  onexlimgt  42454  omabs2  42544  tfsconcatrnss12  42561  rclexi  42828  rtrclex  42830  trclubgNEW  42831  trclexi  42833  rtrclexi  42834  cnvrcl0  42838  cnvtrcl0  42839  dfrtrcl5  42842  trrelsuperrel2dg  42884  dfrcl2  42887  relexp0a  42929  relexpaddss  42931  trclimalb2  42939  frege83d  42961  frege131d  42977  dssmapnvod  43233  clsk3nimkb  43253  isotone1  43261  grumnudlem  43506  infxrpnf  44614  mccllem  44771  cncfiooicclem1  45067  dvmptfprod  45119  dvnprodlem1  45120  iblsplit  45140  fourierdlem54  45334  fourierdlem102  45382  fourierdlem103  45383  fourierdlem104  45384  fourierdlem114  45394  sge0resplit  45580  sge0split  45583  sge0splitmpt  45585  sge0xaddlem1  45607  isomenndlem  45704  hoiprodp1  45762  hoidmvlelem1  45769  hoidmvlelem2  45770  hoidmvlelem3  45771  hoidmvlelem4  45772  gsumsplit2f  47016  setrec1lem4  47896  elpglem2  47918