Theorem ssun1 4158

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

Syntax hints:   ∨ wo 847   ∈ wcel 2109   ∪ cun 3929   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948

This theorem is referenced by:  ssun2  4159  ssun3  4160  elun1  4162  difsssymdif  4243  inabs  4246  reuun1  4308  un00  4425  pwunss  4598  pwundif  4604  snsspr1  4795  snsstp1  4797  snsstp2  4798  uniintsn  4966  sofld  6181  sssucid  6439  fvrn0  6911  f1ounsn  7270  ovima0  7591  unexb  7746  unexbOLD  7747  dmexg  7902  resf1extb  7935  xpord2indlem  8151  xpord3inddlem  8158  suppun  8188  dftpos2  8247  tpostpos2  8251  frrlem12  8301  frrlem13  8302  wfrlem14OLD  8341  wfrlem15OLD  8342  tfrlem11  8407  oaabs2  8666  ralxpmap  8915  domss2  9155  mapunen  9165  ac6sfi  9297  frfi  9298  unfir  9323  domunfican  9338  iunfi  9360  elfiun  9447  dffi3  9448  unwdomg  9603  unxpwdom2  9607  unxpwdom  9608  cantnfp1lem1  9697  cantnfp1lem3  9699  tc2  9761  unwf  9829  rankunb  9869  r0weon  10031  infxpenlem  10032  dfac2b  10150  djudoml  10204  cdainflem  10207  infunabs  10225  infdju  10226  infdif  10227  ackbij1lem15  10252  cfsmolem  10289  isfin4p1  10334  fin23lem11  10336  fin1a2lem10  10428  fin1a2lem13  10431  axdc3lem4  10472  axcclem  10476  zornn0g  10524  ttukeylem1  10528  ttukeylem5  10532  ttukeylem7  10534  fingch  10642  fpwwe2lem12  10661  gchac  10700  wunfi  10740  wundm  10747  wunex2  10757  inar1  10794  ressxr  11284  nnssnn0  12509  un0addcl  12539  un0mulcl  12540  nn0ssxnn0  12582  hashbclem  14475  hashf1lem1  14478  hashf1lem2  14479  ccatrn  14612  trclublem  15019  relexpdmg  15066  relexpaddg  15077  fsumsplit  15762  fsum2d  15792  fsumabs  15822  fsumrlim  15832  fsumo1  15833  incexclem  15857  fprodsplit  15987  fprod2d  16002  lcmfunsnlem1  16661  coprmprod  16685  vdwapid1  17000  vdwlem6  17011  ramcl2  17041  isstruct2  17173  srngbase  17329  srngplusg  17330  srngmulr  17331  lmodbase  17345  lmodplusg  17346  lmodsca  17347  ipsbase  17356  ipsaddg  17357  ipsmulr  17358  phlbase  17366  phlplusg  17367  phlsca  17368  odrngbas  17423  odrngplusg  17424  odrngmulr  17425  prdssca  17475  prdsbas  17476  prdsplusg  17477  prdsmulr  17478  prdsvsca  17479  prdsip  17480  prdsle  17481  prdsds  17483  prdstset  17485  imasbas  17531  imasplusg  17536  imasmulr  17537  imassca  17538  imasvsca  17539  imasip  17540  mreexexlem2d  17662  drsdirfi  18322  ipobas  18546  ipotset  18548  acsfiindd  18568  psdmrn  18588  dirdm  18615  grpinvfval  18966  mulgfval  19057  gsumzsplit  19913  gsumsplit2  19915  gsumzunsnd  19942  gsum2dlem2  19957  dprdfadd  20008  dmdprdsplit2lem  20033  dmdprdsplit2  20034  dmdprdsplit  20035  dprdsplit  20036  ablfac1eulem  20060  lspun  20949  lspsolv  21109  lsppratlem3  21115  islbs3  21121  lbsextlem2  21125  lbsextlem4  21127  cnfldbas  21324  mpocnfldadd  21325  mpocnfldmul  21327  cnfldcj  21329  cnfldtset  21330  cnfldle  21331  cnfldds  21332  cnfldbasOLD  21339  cnfldaddOLD  21340  cnfldmulOLD  21341  cnfldcjOLD  21342  cnfldtsetOLD  21343  cnfldleOLD  21344  cnflddsOLD  21345  psrbas  21898  psrplusg  21901  psrmulr  21907  mplsubglem  21964  mplcoe1  22000  mplcoe5  22003  mdetunilem9  22563  basdif0  22896  ordtbas2  23134  ordtbas  23135  ordtopn1  23137  leordtval2  23155  iocpnfordt  23158  icomnfordt  23159  uncmp  23346  fiuncmp  23347  bwth  23353  locfincmp  23469  comppfsc  23475  1stckgenlem  23496  1stckgen  23497  ptbasin  23520  ptbasfi  23524  dfac14lem  23560  dfac14  23561  ptuncnv  23750  ptunhmeo  23751  ptcmpfi  23756  fbun  23783  trfil2  23830  ufprim  23852  ufileu  23862  filufint  23863  ufildr  23874  fmfnfm  23901  hausflim  23924  fclsfnflim  23970  alexsubALTlem4  23993  tmdgsum  24038  tsmsgsum  24082  tsmsres  24087  tsmssplit  24095  tsmsxplem1  24096  ustssco  24158  ustuqtop1  24185  prdsxmetlem  24312  prdsbl  24435  icccmplem2  24768  fsumcn  24817  cnmpopc  24878  rrxmetlem  25364  rrxmet  25365  rrxdstprj1  25366  ovolctb2  25450  ovolunnul  25458  ovolfiniun  25459  nulmbl2  25494  finiunmbl  25502  volfiniun  25505  icombl  25522  ioombl  25523  uniiccdif  25536  mbfres2  25603  itg2splitlem  25706  itg2split  25707  itgfsum  25785  itgsplit  25794  itgsplitioo  25796  dvreslem  25867  dvaddbr  25897  dvmulbr  25898  dvmulbrOLD  25899  dvmptfsum  25936  lhop  25978  dvcnvrelem2  25980  mdegcl  26031  elplyr  26163  plyrem  26270  xrlimcnp  26935  fsumharmonic  26979  chtdif  27125  lgsdir2lem3  27295  lgsquadlem2  27349  dchrisum0lem1b  27483  pntrlog2bndlem6  27551  pntlemf  27573  nosupinfsep  27701  noetalem1  27710  scutun12  27779  cofcutrtime  27892  addsuniflem  27965  addsbday  27981  negsval  27988  mulsproplem12  28087  mulsproplem13  28088  mulsproplem14  28089  mulsuniflem  28109  mulsass  28126  precsexlem6  28171  precsexlem7  28172  precsexlem10  28175  precsexlem11  28176  ex-ss  30413  shsleji  31356  shsval2i  31373  ssjo  31433  sshhococi  31532  padct  32702  gsumle  33097  symgcom  33099  cycpmco2lem5  33146  cycpmco2lem6  33147  cycpmco2lem7  33148  cycpmco2  33149  gsumvsca1  33228  gsumvsca2  33229  elrgspnsubrunlem1  33247  rlocbas  33267  rlocaddval  33268  rlocmulval  33269  elrspunsn  33449  mxidlprm  33490  idlsrgbas  33524  idlsrgplusg  33525  idlsrgmulr  33527  fldextrspundgdvdslem  33726  fldextrspundgdvds  33727  constrextdg2lem  33787  esumsplit  34089  esumpad2  34092  aean  34280  sxbrsigalem2  34323  bnj931  34806  subfacp1lem2b  35208  subfacp1lem3  35209  subfacp1lem5  35211  kur14lem7  35239  kur14lem9  35241  cvmliftlem10  35321  satfsschain  35391  fmlasssuc  35416  refssfne  36381  filnetlem3  36403  bj-unrab  36949  bj-snglsstag  37004  bj-2upln0  37046  bj-ccssccbar  37240  rdgssun  37401  finixpnum  37634  matunitlindflem1  37645  mbfresfi  37695  prdsbnd  37822  heibor1lem  37838  rrnequiv  37864  paddunssN  39832  sspadd1  39839  sspadd2  39840  pclfinN  39924  dochdmj1  41414  dvhdimlem  41468  elrfi  42692  mzpcompact2lem  42749  eldioph2  42760  eldioph4b  42809  ttac  43035  pwssplit4  43088  pwslnmlem2  43092  isnumbasgrplem2  43103  algbase  43173  algaddg  43174  algmulr  43175  fiuneneq  43191  idomsubgmo  43192  onexlimgt  43242  omabs2  43331  tfsconcatrnss12  43348  rclexi  43614  rtrclex  43616  trclubgNEW  43617  trclexi  43619  rtrclexi  43620  cnvrcl0  43624  cnvtrcl0  43625  dfrtrcl5  43628  trrelsuperrel2dg  43670  dfrcl2  43673  relexp0a  43715  relexpaddss  43717  trclimalb2  43725  frege83d  43747  frege131d  43763  dssmapnvod  44019  clsk3nimkb  44039  isotone1  44047  grumnudlem  44284  dmwf  44965  infxrpnf  45453  mccllem  45606  cncfiooicclem1  45902  dvmptfprod  45954  dvnprodlem1  45955  iblsplit  45975  fourierdlem54  46169  fourierdlem102  46217  fourierdlem103  46218  fourierdlem104  46219  fourierdlem114  46229  sge0resplit  46415  sge0split  46418  sge0splitmpt  46420  sge0xaddlem1  46442  isomenndlem  46539  hoiprodp1  46597  hoidmvlelem1  46604  hoidmvlelem2  46605  hoidmvlelem3  46606  hoidmvlelem4  46607  dfnbgrss2  47852  gsumsplit2f  48135  setrec1lem4  49534  elpglem2  49556