Theorem ssun1 4102

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 863	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 4079	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 233	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3921	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 843   ∈ wcel 2108   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  ssun2  4103  ssun3  4104  elun1  4106  difsssymdif  4183  inabs  4186  reuun1  4248  un00  4373  pwunss  4550  pwundif  4556  snsspr1  4744  snsstp1  4746  snsstp2  4747  uniintsn  4915  sofld  6079  sssucid  6328  fvrn0  6784  ovima0  7429  unexb  7576  dmexg  7724  suppun  7971  dftpos2  8030  tpostpos2  8034  frrlem12  8084  frrlem13  8085  wfrlem14OLD  8124  wfrlem15OLD  8125  tfrlem11  8190  oaabs2  8439  ralxpmap  8642  domss2  8872  mapunen  8882  ac6sfi  8988  frfi  8989  unfir  9012  domunfican  9017  iunfi  9037  elfiun  9119  dffi3  9120  unwdomg  9273  unxpwdom2  9277  unxpwdom  9278  cantnfp1lem1  9366  cantnfp1lem3  9368  dftrpred3g  9412  tc2  9431  unwf  9499  rankunb  9539  r0weon  9699  infxpenlem  9700  dfac2b  9817  djudoml  9871  cdainflem  9874  infunabs  9894  infdju  9895  infdif  9896  ackbij1lem15  9921  cfsmolem  9957  isfin4p1  10002  fin23lem11  10004  fin1a2lem10  10096  fin1a2lem13  10099  axdc3lem4  10140  axcclem  10144  zornn0g  10192  ttukeylem1  10196  ttukeylem5  10200  ttukeylem7  10202  fingch  10310  fpwwe2lem12  10329  gchac  10368  wunfi  10408  wundm  10415  wunex2  10425  inar1  10462  ressxr  10950  nnssnn0  12166  un0addcl  12196  un0mulcl  12197  nn0ssxnn0  12238  hashbclem  14092  hashf1lem1  14096  hashf1lem1OLD  14097  hashf1lem2  14098  ccatrn  14222  trclublem  14634  relexpdmg  14681  relexpaddg  14692  fsumsplit  15381  fsum2d  15411  fsumabs  15441  fsumrlim  15451  fsumo1  15452  incexclem  15476  fprodsplit  15604  fprod2d  15619  lcmfunsnlem1  16270  coprmprod  16294  vdwapid1  16604  vdwlem6  16615  ramcl2  16645  isstruct2  16778  srngbase  16946  srngplusg  16947  srngmulr  16948  lmodbase  16962  lmodplusg  16963  lmodsca  16964  ipsbase  16972  ipsaddg  16973  ipsmulr  16974  phlbase  16982  phlplusg  16983  phlsca  16984  odrngbas  17033  odrngplusg  17034  odrngmulr  17035  prdssca  17084  prdsbas  17085  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  prdsip  17089  prdsle  17090  prdsds  17092  prdstset  17094  imasbas  17140  imasplusg  17145  imasmulr  17146  imassca  17147  imasvsca  17148  imasip  17149  mreexexlem2d  17271  drsdirfi  17938  ipobas  18164  ipotset  18166  acsfiindd  18186  psdmrn  18206  dirdm  18233  grpinvfval  18533  mulgfval  18617  gsumzsplit  19443  gsumsplit2  19445  gsumzunsnd  19472  gsum2dlem2  19487  dprdfadd  19538  dmdprdsplit2lem  19563  dmdprdsplit2  19564  dmdprdsplit  19565  dprdsplit  19566  ablfac1eulem  19590  lspun  20164  lspsolv  20320  lsppratlem3  20326  islbs3  20332  lbsextlem2  20336  lbsextlem4  20338  cnfldbas  20514  cnfldadd  20515  cnfldmul  20516  cnfldcj  20517  cnfldtset  20518  cnfldle  20519  cnfldds  20520  psrbagaddclOLD  21042  psrbas  21057  psrplusg  21060  psrmulr  21063  mplsubglem  21115  mplcoe1  21148  mplcoe5  21151  mdetunilem9  21677  basdif0  22011  ordtbas2  22250  ordtbas  22251  ordtopn1  22253  leordtval2  22271  iocpnfordt  22274  icomnfordt  22275  uncmp  22462  fiuncmp  22463  bwth  22469  locfincmp  22585  comppfsc  22591  1stckgenlem  22612  1stckgen  22613  ptbasin  22636  ptbasfi  22640  dfac14lem  22676  dfac14  22677  ptuncnv  22866  ptunhmeo  22867  ptcmpfi  22872  fbun  22899  trfil2  22946  ufprim  22968  ufileu  22978  filufint  22979  ufildr  22990  fmfnfm  23017  hausflim  23040  fclsfnflim  23086  alexsubALTlem4  23109  tmdgsum  23154  tsmsgsum  23198  tsmsres  23203  tsmssplit  23211  tsmsxplem1  23212  ustssco  23274  ustuqtop1  23301  prdsxmetlem  23429  prdsbl  23553  icccmplem2  23892  fsumcn  23939  cnmpopc  23997  rrxmetlem  24476  rrxmet  24477  rrxdstprj1  24478  ovolctb2  24561  ovolunnul  24569  ovolfiniun  24570  nulmbl2  24605  finiunmbl  24613  volfiniun  24616  icombl  24633  ioombl  24634  uniiccdif  24647  mbfres2  24714  itg2splitlem  24818  itg2split  24819  itgfsum  24896  itgsplit  24905  itgsplitioo  24907  dvreslem  24978  dvaddbr  25007  dvmulbr  25008  dvmptfsum  25044  lhop  25085  dvcnvrelem2  25087  mdegcl  25139  elplyr  25267  plyrem  25370  xrlimcnp  26023  fsumharmonic  26066  chtdif  26212  lgsdir2lem3  26380  lgsquadlem2  26434  dchrisum0lem1b  26568  pntrlog2bndlem6  26636  pntlemf  26658  ex-ss  28692  shsleji  29633  shsval2i  29650  ssjo  29710  sshhococi  29809  padct  30956  gsumle  31252  symgcom  31254  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  gsumvsca1  31381  gsumvsca2  31382  mxidlprm  31542  idlsrgbas  31551  idlsrgplusg  31552  idlsrgmulr  31554  esumsplit  31921  esumpad2  31924  aean  32112  sxbrsigalem2  32153  bnj931  32650  subfacp1lem2b  33043  subfacp1lem3  33044  subfacp1lem5  33046  kur14lem7  33074  kur14lem9  33076  cvmliftlem10  33156  satfsschain  33226  fmlasssuc  33251  xpord2ind  33721  xpord3ind  33727  nosupinfsep  33862  noetalem1  33871  scutun12  33931  cofcutrtime  34020  negsval  34050  refssfne  34474  filnetlem3  34496  bj-unrab  35041  bj-snglsstag  35098  bj-2upln0  35140  bj-ccssccbar  35315  rdgssun  35476  finixpnum  35689  matunitlindflem1  35700  mbfresfi  35750  prdsbnd  35878  heibor1lem  35894  rrnequiv  35920  paddunssN  37749  sspadd1  37756  sspadd2  37757  pclfinN  37841  dochdmj1  39331  dvhdimlem  39385  elrfi  40432  mzpcompact2lem  40489  eldioph2  40500  eldioph4b  40549  ttac  40774  pwssplit4  40830  pwslnmlem2  40834  isnumbasgrplem2  40845  algbase  40919  algaddg  40920  algmulr  40921  fiuneneq  40938  idomsubgmo  40939  rclexi  41112  rtrclex  41114  trclubgNEW  41115  trclexi  41117  rtrclexi  41118  cnvrcl0  41122  cnvtrcl0  41123  dfrtrcl5  41126  trrelsuperrel2dg  41168  dfrcl2  41171  relexp0a  41213  relexpaddss  41215  trclimalb2  41223  frege83d  41245  frege131d  41261  dssmapnvod  41517  clsk3nimkb  41539  isotone1  41547  grumnudlem  41792  infxrpnf  42876  mccllem  43028  cncfiooicclem1  43324  dvmptfprod  43376  dvnprodlem1  43377  iblsplit  43397  fourierdlem54  43591  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  sge0resplit  43834  sge0split  43837  sge0splitmpt  43839  sge0xaddlem1  43861  isomenndlem  43958  hoiprodp1  44016  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  gsumsplit2f  45262  setrec1lem4  46282  elpglem2  46303