Theorem ssun1 4118

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 868	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 4093	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 234	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3925	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 848   ∈ wcel 2114   ∪ cun 3887   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906

This theorem is referenced by:  ssun2  4119  ssun3  4120  elun1  4122  difsssymdif  4203  inabs  4206  reuun1  4268  un00  4385  pwunss  4559  pwundif  4565  snsspr1  4757  snsstp1  4759  snsstp2  4760  uniintsn  4927  sofld  6151  sssucid  6405  fvrn0  6868  f1ounsn  7227  ovima0  7546  unexb  7701  unexbOLD  7702  dmexg  7852  resf1extb  7885  xpord2indlem  8097  xpord3inddlem  8104  suppun  8134  dftpos2  8193  tpostpos2  8197  frrlem12  8247  frrlem13  8248  tfrlem11  8327  oaabs2  8585  ralxpmap  8844  domss2  9074  mapunen  9084  ac6sfi  9194  frfi  9195  unfir  9218  domunfican  9232  iunfi  9253  elfiun  9343  dffi3  9344  unwdomg  9499  unxpwdom2  9503  unxpwdom  9504  cantnfp1lem1  9599  cantnfp1lem3  9601  tc2  9661  unwf  9734  rankunb  9774  r0weon  9934  infxpenlem  9935  dfac2b  10053  djudoml  10107  cdainflem  10110  infunabs  10128  infdju  10129  infdif  10130  ackbij1lem15  10155  cfsmolem  10192  isfin4p1  10237  fin23lem11  10239  fin1a2lem10  10331  fin1a2lem13  10334  axdc3lem4  10375  axcclem  10379  zornn0g  10427  ttukeylem1  10431  ttukeylem5  10435  ttukeylem7  10437  fingch  10546  fpwwe2lem12  10565  gchac  10604  wunfi  10644  wundm  10651  wunex2  10661  inar1  10698  ressxr  11189  nnssnn0  12440  un0addcl  12470  un0mulcl  12471  nn0ssxnn0  12513  hashbclem  14414  hashf1lem1  14417  hashf1lem2  14418  ccatrn  14552  trclublem  14957  relexpdmg  15004  relexpaddg  15015  fsumsplit  15703  fsum2d  15733  fsumabs  15764  fsumrlim  15774  fsumo1  15775  incexclem  15801  fprodsplit  15931  fprod2d  15946  lcmfunsnlem1  16606  coprmprod  16630  vdwapid1  16946  vdwlem6  16957  ramcl2  16987  isstruct2  17119  srngbase  17273  srngplusg  17274  srngmulr  17275  lmodbase  17289  lmodplusg  17290  lmodsca  17291  ipsbase  17300  ipsaddg  17301  ipsmulr  17302  phlbase  17310  phlplusg  17311  phlsca  17312  odrngbas  17367  odrngplusg  17368  odrngmulr  17369  prdssca  17419  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdsip  17424  prdsle  17425  prdsds  17427  prdstset  17429  imasbas  17476  imasplusg  17481  imasmulr  17482  imassca  17483  imasvsca  17484  imasip  17485  mreexexlem2d  17611  drsdirfi  18271  ipobas  18497  ipotset  18499  acsfiindd  18519  psdmrn  18539  dirdm  18566  grpinvfval  18954  mulgfval  19045  gsumzsplit  19902  gsumsplit2  19904  gsumzunsnd  19931  gsum2dlem2  19946  dprdfadd  19997  dmdprdsplit2lem  20022  dmdprdsplit2  20023  dmdprdsplit  20024  dprdsplit  20025  ablfac1eulem  20049  gsumle  20120  lspun  20982  lspsolv  21141  lsppratlem3  21147  islbs3  21153  lbsextlem2  21157  lbsextlem4  21159  cnfldbas  21356  mpocnfldadd  21357  mpocnfldmul  21359  cnfldcj  21361  cnfldtset  21362  cnfldle  21363  cnfldds  21364  psrbas  21913  psrplusg  21916  psrmulr  21921  mplsubglem  21977  mplcoe1  22015  mplcoe5  22018  mdetunilem9  22585  basdif0  22918  ordtbas2  23156  ordtbas  23157  ordtopn1  23159  leordtval2  23177  iocpnfordt  23180  icomnfordt  23181  uncmp  23368  fiuncmp  23369  bwth  23375  locfincmp  23491  comppfsc  23497  1stckgenlem  23518  1stckgen  23519  ptbasin  23542  ptbasfi  23546  dfac14lem  23582  dfac14  23583  ptuncnv  23772  ptunhmeo  23773  ptcmpfi  23778  fbun  23805  trfil2  23852  ufprim  23874  ufileu  23884  filufint  23885  ufildr  23896  fmfnfm  23923  hausflim  23946  fclsfnflim  23992  alexsubALTlem4  24015  tmdgsum  24060  tsmsgsum  24104  tsmsres  24109  tsmssplit  24117  tsmsxplem1  24118  ustssco  24180  ustuqtop1  24206  prdsxmetlem  24333  prdsbl  24456  icccmplem2  24789  fsumcn  24837  cnmpopc  24895  rrxmetlem  25374  rrxmet  25375  rrxdstprj1  25376  ovolctb2  25459  ovolunnul  25467  ovolfiniun  25468  nulmbl2  25503  finiunmbl  25511  volfiniun  25514  icombl  25531  ioombl  25532  uniiccdif  25545  mbfres2  25612  itg2splitlem  25715  itg2split  25716  itgfsum  25794  itgsplit  25803  itgsplitioo  25805  dvreslem  25876  dvaddbr  25905  dvmulbr  25906  dvmptfsum  25942  lhop  25983  dvcnvrelem2  25985  mdegcl  26034  elplyr  26166  plyrem  26271  xrlimcnp  26932  fsumharmonic  26975  chtdif  27121  lgsdir2lem3  27290  lgsquadlem2  27344  dchrisum0lem1b  27478  pntrlog2bndlem6  27546  pntlemf  27568  nosupinfsep  27696  noetalem1  27705  cutsun12  27782  cofcutrtime  27919  addsuniflem  27993  addbday  28010  negsval  28017  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  mulsuniflem  28141  mulsass  28158  precsexlem6  28204  precsexlem7  28205  precsexlem10  28208  precsexlem11  28209  ex-ss  30497  shsleji  31441  shsval2i  31458  ssjo  31518  sshhococi  31617  padct  32791  symgcom  33144  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  gsumvsca1  33287  gsumvsca2  33288  elrgspnsubrunlem1  33308  rlocbas  33328  rlocaddval  33329  rlocmulval  33330  elrspunsn  33489  mxidlprm  33530  idlsrgbas  33564  idlsrgplusg  33565  idlsrgmulr  33567  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  constrextdg2lem  33892  esumsplit  34197  esumpad2  34200  aean  34388  sxbrsigalem2  34430  bnj931  34913  tz9.1regs  35278  subfacp1lem2b  35363  subfacp1lem3  35364  subfacp1lem5  35366  kur14lem7  35394  kur14lem9  35396  cvmliftlem10  35476  satfsschain  35546  fmlasssuc  35571  refssfne  36540  filnetlem3  36562  bj-unrab  37233  bj-snglsstag  37288  bj-2upln0  37330  bj-ccssccbar  37531  rdgssun  37694  finixpnum  37926  matunitlindflem1  37937  mbfresfi  37987  prdsbnd  38114  heibor1lem  38130  rrnequiv  38156  paddunssN  40254  sspadd1  40261  sspadd2  40262  pclfinN  40346  dochdmj1  41836  dvhdimlem  41890  elrfi  43126  mzpcompact2lem  43183  eldioph2  43194  eldioph4b  43239  ttac  43464  pwssplit4  43517  pwslnmlem2  43521  isnumbasgrplem2  43532  algbase  43602  algaddg  43603  algmulr  43604  fiuneneq  43620  idomsubgmo  43621  onexlimgt  43671  omabs2  43760  tfsconcatrnss12  43777  rclexi  44042  rtrclex  44044  trclubgNEW  44045  trclexi  44047  rtrclexi  44048  cnvrcl0  44052  cnvtrcl0  44053  dfrtrcl5  44056  trrelsuperrel2dg  44098  dfrcl2  44101  relexp0a  44143  relexpaddss  44145  trclimalb2  44153  frege83d  44175  frege131d  44191  dssmapnvod  44447  clsk3nimkb  44467  isotone1  44475  grumnudlem  44712  dmwf  45392  infxrpnf  45874  mccllem  46027  cncfiooicclem1  46321  dvmptfprod  46373  dvnprodlem1  46374  iblsplit  46394  fourierdlem54  46588  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  sge0resplit  46834  sge0split  46837  sge0splitmpt  46839  sge0xaddlem1  46861  isomenndlem  46958  hoiprodp1  47016  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  dfnbgrss2  48335  gsumsplit2f  48656  setrec1lem4  50165  elpglem2  50187