Theorem ssun1 4187

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

Syntax hints:   ∨ wo 847   ∈ wcel 2105   ∪ cun 3960   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979

This theorem is referenced by:  ssun2  4188  ssun3  4189  elun1  4191  difsssymdif  4268  inabs  4271  reuun1  4333  un00  4450  pwunss  4622  pwundif  4628  snsspr1  4818  snsstp1  4820  snsstp2  4821  uniintsn  4989  sofld  6208  sssucid  6465  fvrn0  6936  f1ounsn  7291  ovima0  7611  unexb  7765  unexbOLD  7766  dmexg  7923  xpord2indlem  8170  xpord3inddlem  8177  suppun  8207  dftpos2  8266  tpostpos2  8270  frrlem12  8320  frrlem13  8321  wfrlem14OLD  8360  wfrlem15OLD  8361  tfrlem11  8426  oaabs2  8685  ralxpmap  8934  domss2  9174  mapunen  9184  ac6sfi  9317  frfi  9318  unfir  9343  domunfican  9358  iunfi  9380  elfiun  9467  dffi3  9468  unwdomg  9621  unxpwdom2  9625  unxpwdom  9626  cantnfp1lem1  9715  cantnfp1lem3  9717  tc2  9779  unwf  9847  rankunb  9887  r0weon  10049  infxpenlem  10050  dfac2b  10168  djudoml  10222  cdainflem  10225  infunabs  10243  infdju  10244  infdif  10245  ackbij1lem15  10270  cfsmolem  10307  isfin4p1  10352  fin23lem11  10354  fin1a2lem10  10446  fin1a2lem13  10449  axdc3lem4  10490  axcclem  10494  zornn0g  10542  ttukeylem1  10546  ttukeylem5  10550  ttukeylem7  10552  fingch  10660  fpwwe2lem12  10679  gchac  10718  wunfi  10758  wundm  10765  wunex2  10775  inar1  10812  ressxr  11302  nnssnn0  12526  un0addcl  12556  un0mulcl  12557  nn0ssxnn0  12599  hashbclem  14487  hashf1lem1  14490  hashf1lem2  14491  ccatrn  14623  trclublem  15030  relexpdmg  15077  relexpaddg  15088  fsumsplit  15773  fsum2d  15803  fsumabs  15833  fsumrlim  15843  fsumo1  15844  incexclem  15868  fprodsplit  15998  fprod2d  16013  lcmfunsnlem1  16670  coprmprod  16694  vdwapid1  17008  vdwlem6  17019  ramcl2  17049  isstruct2  17182  srngbase  17355  srngplusg  17356  srngmulr  17357  lmodbase  17371  lmodplusg  17372  lmodsca  17373  ipsbase  17382  ipsaddg  17383  ipsmulr  17384  phlbase  17392  phlplusg  17393  phlsca  17394  odrngbas  17449  odrngplusg  17450  odrngmulr  17451  prdssca  17502  prdsbas  17503  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdsip  17507  prdsle  17508  prdsds  17510  prdstset  17512  imasbas  17558  imasplusg  17563  imasmulr  17564  imassca  17565  imasvsca  17566  imasip  17567  mreexexlem2d  17689  drsdirfi  18362  ipobas  18588  ipotset  18590  acsfiindd  18610  psdmrn  18630  dirdm  18657  grpinvfval  19008  mulgfval  19099  gsumzsplit  19959  gsumsplit2  19961  gsumzunsnd  19988  gsum2dlem2  20003  dprdfadd  20054  dmdprdsplit2lem  20079  dmdprdsplit2  20080  dmdprdsplit  20081  dprdsplit  20082  ablfac1eulem  20106  lspun  21002  lspsolv  21162  lsppratlem3  21168  islbs3  21174  lbsextlem2  21178  lbsextlem4  21180  cnfldbas  21385  mpocnfldadd  21386  mpocnfldmul  21388  cnfldcj  21390  cnfldtset  21391  cnfldle  21392  cnfldds  21393  cnfldbasOLD  21400  cnfldaddOLD  21401  cnfldmulOLD  21402  cnfldcjOLD  21403  cnfldtsetOLD  21404  cnfldleOLD  21405  cnflddsOLD  21406  psrbas  21970  psrplusg  21973  psrmulr  21979  mplsubglem  22036  mplcoe1  22072  mplcoe5  22075  mdetunilem9  22641  basdif0  22975  ordtbas2  23214  ordtbas  23215  ordtopn1  23217  leordtval2  23235  iocpnfordt  23238  icomnfordt  23239  uncmp  23426  fiuncmp  23427  bwth  23433  locfincmp  23549  comppfsc  23555  1stckgenlem  23576  1stckgen  23577  ptbasin  23600  ptbasfi  23604  dfac14lem  23640  dfac14  23641  ptuncnv  23830  ptunhmeo  23831  ptcmpfi  23836  fbun  23863  trfil2  23910  ufprim  23932  ufileu  23942  filufint  23943  ufildr  23954  fmfnfm  23981  hausflim  24004  fclsfnflim  24050  alexsubALTlem4  24073  tmdgsum  24118  tsmsgsum  24162  tsmsres  24167  tsmssplit  24175  tsmsxplem1  24176  ustssco  24238  ustuqtop1  24265  prdsxmetlem  24393  prdsbl  24519  icccmplem2  24858  fsumcn  24907  cnmpopc  24968  rrxmetlem  25454  rrxmet  25455  rrxdstprj1  25456  ovolctb2  25540  ovolunnul  25548  ovolfiniun  25549  nulmbl2  25584  finiunmbl  25592  volfiniun  25595  icombl  25612  ioombl  25613  uniiccdif  25626  mbfres2  25693  itg2splitlem  25797  itg2split  25798  itgfsum  25876  itgsplit  25885  itgsplitioo  25887  dvreslem  25958  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvmptfsum  26027  lhop  26069  dvcnvrelem2  26071  mdegcl  26122  elplyr  26254  plyrem  26361  xrlimcnp  27025  fsumharmonic  27069  chtdif  27215  lgsdir2lem3  27385  lgsquadlem2  27439  dchrisum0lem1b  27573  pntrlog2bndlem6  27641  pntlemf  27663  nosupinfsep  27791  noetalem1  27800  scutun12  27869  cofcutrtime  27975  addsuniflem  28048  addsbday  28064  negsval  28071  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  mulsuniflem  28189  mulsass  28206  precsexlem6  28250  precsexlem7  28251  precsexlem10  28254  precsexlem11  28255  ex-ss  30455  shsleji  31398  shsval2i  31415  ssjo  31475  sshhococi  31574  padct  32736  gsumle  33083  symgcom  33085  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  gsumvsca1  33214  gsumvsca2  33215  rlocbas  33253  rlocaddval  33254  rlocmulval  33255  elrspunsn  33436  mxidlprm  33477  idlsrgbas  33511  idlsrgplusg  33512  idlsrgmulr  33514  esumsplit  34033  esumpad2  34036  aean  34224  sxbrsigalem2  34267  bnj931  34762  subfacp1lem2b  35165  subfacp1lem3  35166  subfacp1lem5  35168  kur14lem7  35196  kur14lem9  35198  cvmliftlem10  35278  satfsschain  35348  fmlasssuc  35373  refssfne  36340  filnetlem3  36362  bj-unrab  36908  bj-snglsstag  36963  bj-2upln0  37005  bj-ccssccbar  37199  rdgssun  37360  finixpnum  37591  matunitlindflem1  37602  mbfresfi  37652  prdsbnd  37779  heibor1lem  37795  rrnequiv  37821  paddunssN  39790  sspadd1  39797  sspadd2  39798  pclfinN  39882  dochdmj1  41372  dvhdimlem  41426  elrfi  42681  mzpcompact2lem  42738  eldioph2  42749  eldioph4b  42798  ttac  43024  pwssplit4  43077  pwslnmlem2  43081  isnumbasgrplem2  43092  algbase  43162  algaddg  43163  algmulr  43164  fiuneneq  43180  idomsubgmo  43181  onexlimgt  43231  omabs2  43321  tfsconcatrnss12  43338  rclexi  43604  rtrclex  43606  trclubgNEW  43607  trclexi  43609  rtrclexi  43610  cnvrcl0  43614  cnvtrcl0  43615  dfrtrcl5  43618  trrelsuperrel2dg  43660  dfrcl2  43663  relexp0a  43705  relexpaddss  43707  trclimalb2  43715  frege83d  43737  frege131d  43753  dssmapnvod  44009  clsk3nimkb  44029  isotone1  44037  grumnudlem  44280  dmwf  44939  infxrpnf  45395  mccllem  45552  cncfiooicclem1  45848  dvmptfprod  45900  dvnprodlem1  45901  iblsplit  45921  fourierdlem54  46115  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  sge0resplit  46361  sge0split  46364  sge0splitmpt  46366  sge0xaddlem1  46388  isomenndlem  46485  hoiprodp1  46543  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  dfnbgrss2  47782  gsumsplit2f  48023  setrec1lem4  48920  elpglem2  48942