Theorem ssun1 4139

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 880	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 4115	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 237	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3949	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 860   ∈ wcel 2149   ∪ cun 3911   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930

This theorem is referenced by:  ssun2  4140  ssun3  4141  elun1  4143  difsssymdif  4224  inabs  4227  reuun1  4289  un00  4370  pwunss  4585  pwundif  4592  snsspr1  4784  snsstp1  4786  snsstp2  4787  uniintsn  4954  sofld  6188  sssucid  6446  fvrn0  6912  f1ounsn  7273  ovima0  7592  unexb  7748  unexbOLD  7749  dmexg  7900  resf1extb  7933  xpord2indlem  8145  xpord3inddlem  8152  suppun  8182  dftpos2  8241  tpostpos2  8245  frrlem12  8296  frrlem13  8297  tfrlem11  8377  oaabs2  8637  ralxpmap  8896  domss2  9126  mapunen  9136  ac6sfi  9246  frfi  9247  unfir  9270  domunfican  9283  iunfi  9302  elfiun  9392  dffi3  9393  unwdomg  9548  unxpwdom2  9552  unxpwdom  9553  cantnfp1lem1  9649  cantnfp1lem3  9651  tc2  9711  unwf  9784  rankunb  9824  r0weon  9998  infxpenlem  9999  dfac2b  10116  djudoml  10170  cdainflem  10173  infunabs  10191  infdju  10192  infdif  10193  ackbij1lem15  10218  cfsmolem  10256  isfin4p1  10301  fin23lem11  10303  fin1a2lem10  10395  fin1a2lem13  10398  axdc3lem4  10439  axcclem  10443  zornn0g  10491  ttukeylem1  10495  ttukeylem5  10499  ttukeylem7  10501  fingch  10610  fpwwe2lem12  10629  gchac  10668  wunfi  10708  wundm  10715  wunex2  10725  inar1  10762  ressxr  11255  nnssnn0  12509  un0addcl  12539  un0mulcl  12540  nn0ssxnn0  12582  hashbclem  14491  hashf1lem1  14494  hashf1lem2  14495  ccatrn  14629  trclublem  15034  relexpdmg  15081  relexpaddg  15092  fsumsplit  15794  fsum2d  15824  fsumabs  15855  fsumrlim  15865  fsumo1  15866  incexclem  15892  fprodsplit  16022  fprod2d  16037  lcmfunsnlem1  16697  coprmprod  16721  vdwapid1  17037  vdwlem6  17048  ramcl2  17078  isstruct2  17211  srngbase  17365  srngplusg  17366  srngmulr  17367  lmodbase  17381  lmodplusg  17382  lmodsca  17383  ipsbase  17392  ipsaddg  17393  ipsmulr  17394  phlbase  17402  phlplusg  17403  phlsca  17404  odrngbas  17459  odrngplusg  17460  odrngmulr  17461  prdssca  17511  prdsbas  17512  prdsplusg  17513  prdsmulr  17514  prdsvsca  17515  prdsip  17516  prdsle  17517  prdsds  17519  prdstset  17521  imasbas  17568  imasplusg  17573  imasmulr  17574  imassca  17575  imasvsca  17576  imasip  17577  mreexexlem2d  17703  drsdirfi  18363  ipobas  18589  ipotset  18591  acsfiindd  18611  psdmrn  18631  dirdm  18658  grpinvfval  19047  mulgfval  19137  gsumzsplit  19999  gsumsplit2  20001  gsumzunsnd  20028  gsum2dlem2  20043  dprdfadd  20094  dmdprdsplit2lem  20119  dmdprdsplit2  20120  dmdprdsplit  20121  dprdsplit  20122  ablfac1eulem  20146  gsumle  20217  lspun  21088  lspsolv  21247  lsppratlem3  21253  islbs3  21259  lbsextlem2  21263  lbsextlem4  21265  cnfldbas  21497  mpocnfldadd  21498  mpocnfldmul  21500  cnfldcj  21502  cnfldtset  21503  cnfldle  21504  cnfldds  21505  psrbas  22055  psrplusg  22058  psrmulr  22063  mplsubglem  22119  mplcoe1  22159  mplcoe5  22162  mdetunilem9  22748  basdif0  23081  ordtbas2  23319  ordtbas  23320  ordtopn1  23322  leordtval2  23340  iocpnfordt  23343  icomnfordt  23344  uncmp  23531  fiuncmp  23532  bwth  23538  locfincmp  23654  comppfsc  23660  1stckgenlem  23681  1stckgen  23682  ptbasin  23705  ptbasfi  23709  dfac14lem  23745  dfac14  23746  ptuncnv  23935  ptunhmeo  23936  ptcmpfi  23941  fbun  23968  trfil2  24015  ufprim  24037  ufileu  24047  filufint  24048  ufildr  24059  fmfnfm  24086  hausflim  24109  fclsfnflim  24155  alexsubALTlem4  24178  tmdgsum  24223  tsmsgsum  24267  tsmsres  24272  tsmssplit  24280  tsmsxplem1  24281  ustssco  24343  ustuqtop1  24369  prdsxmetlem  24496  prdsbl  24619  icccmplem2  24952  fsumcn  25000  cnmpopc  25058  rrxmetlem  25537  rrxmet  25538  rrxdstprj1  25539  ovolctb2  25622  ovolunnul  25630  ovolfiniun  25631  nulmbl2  25666  finiunmbl  25674  volfiniun  25677  icombl  25694  ioombl  25695  uniiccdif  25708  mbfres2  25775  itg2splitlem  25878  itg2split  25879  itgfsum  25957  itgsplit  25966  itgsplitioo  25968  dvreslem  26039  dvaddbr  26068  dvmulbr  26069  dvmptfsum  26105  lhop  26146  dvcnvrelem2  26148  mdegcl  26197  elplyr  26329  plyrem  26437  xrlimcnp  27101  fsumharmonic  27144  chtdif  27290  lgsdir2lem3  27459  lgsquadlem2  27513  dchrisum0lem1b  27647  pntrlog2bndlem6  27715  pntlemf  27737  nosupinfsep  27864  noetalem1  27873  cutsun12  27951  cofcutrtime  28088  addsuniflem  28162  addbday  28179  negsval  28186  mulsproplem12  28288  mulsproplem13  28289  mulsproplem14  28290  mulsuniflem  28310  mulsass  28327  precsexlem6  28373  precsexlem7  28374  precsexlem10  28377  precsexlem11  28378  ex-ss  30721  shsleji  31665  shsval2i  31682  ssjo  31742  sshhococi  31841  padct  33006  symgcom  33346  cycpmco2lem5  33393  cycpmco2lem6  33394  cycpmco2lem7  33395  cycpmco2  33396  gsumvsca1  33489  gsumvsca2  33490  elrgspnsubrunlem1  33510  rlocbas  33531  rlocaddval  33532  rlocmulval  33533  elrspunsn  33683  mxidlprm  33700  idlsrgbas  33741  idlsrgplusg  33742  idlsrgmulr  33744  fldextrspundgdvdslem  34017  fldextrspundgdvds  34018  constrextdg2lem  34085  esumsplit  34390  esumpad2  34393  aean  34581  sxbrsigalem2  34623  bnj931  35106  tz9.1regs  35482  subfacp1lem2b  35608  subfacp1lem3  35609  subfacp1lem5  35611  kur14lem7  35639  kur14lem9  35641  cvmliftlem10  35721  satfsschain  35791  fmlasssuc  35816  refssfne  36794  filnetlem3  36816  bj-unrab  37487  bj-snglsstag  37542  bj-2upln0  37584  bj-ccssccbar  37786  rdgssun  37949  finixpnum  38181  matunitlindflem1  38192  mbfresfi  38242  prdsbnd  38369  heibor1lem  38385  rrnequiv  38411  paddunssN  40509  sspadd1  40516  sspadd2  40517  pclfinN  40601  dochdmj1  42091  dvhdimlem  42145  elrfi  43354  mzpcompact2lem  43411  eldioph2  43422  eldioph4b  43467  ttac  43692  pwssplit4  43745  pwslnmlem2  43749  isnumbasgrplem2  43760  algbase  43830  algaddg  43831  algmulr  43832  fiuneneq  43848  idomsubgmo  43849  onexlimgt  43899  omabs2  43988  tfsconcatrnss12  44005  rclexi  44270  rtrclex  44272  trclubgNEW  44273  trclexi  44275  rtrclexi  44276  cnvrcl0  44280  cnvtrcl0  44281  dfrtrcl5  44284  trrelsuperrel2dg  44326  dfrcl2  44329  relexp0a  44371  relexpaddss  44373  trclimalb2  44381  frege83d  44403  frege131d  44419  dssmapnvod  44675  clsk3nimkb  44695  isotone1  44703  grumnudlem  44924  dmwf  45603  infxrpnf  46089  mccllem  46242  cncfiooicclem1  46536  dvmptfprod  46588  dvnprodlem1  46589  iblsplit  46609  fourierdlem54  46803  fourierdlem102  46851  fourierdlem103  46852  fourierdlem104  46853  fourierdlem114  46863  sge0resplit  47049  sge0split  47052  sge0splitmpt  47054  sge0xaddlem1  47076  isomenndlem  47173  hoiprodp1  47231  hoidmvlelem1  47238  hoidmvlelem2  47239  hoidmvlelem3  47240  hoidmvlelem4  47241  dfnbgrss2  48550  gsumsplit2f  48871  setrec1lem4  50390  elpglem2  50412