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  6186  sssucid  6444  fvrn0  6910  f1ounsn  7271  ovima0  7590  unexb  7745  unexbOLD  7746  dmexg  7897  resf1extb  7930  xpord2indlem  8142  xpord3inddlem  8149  suppun  8179  dftpos2  8238  tpostpos2  8242  frrlem12  8293  frrlem13  8294  tfrlem11  8374  oaabs2  8634  ralxpmap  8893  domss2  9123  mapunen  9133  ac6sfi  9243  frfi  9244  unfir  9267  domunfican  9280  iunfi  9299  elfiun  9389  dffi3  9390  unwdomg  9545  unxpwdom2  9549  unxpwdom  9550  cantnfp1lem1  9646  cantnfp1lem3  9648  tc2  9708  unwf  9781  rankunb  9821  r0weon  9995  infxpenlem  9996  dfac2b  10113  djudoml  10167  cdainflem  10170  infunabs  10188  infdju  10189  infdif  10190  ackbij1lem15  10215  cfsmolem  10253  isfin4p1  10298  fin23lem11  10300  fin1a2lem10  10392  fin1a2lem13  10395  axdc3lem4  10436  axcclem  10440  zornn0g  10488  ttukeylem1  10492  ttukeylem5  10496  ttukeylem7  10498  fingch  10607  fpwwe2lem12  10626  gchac  10665  wunfi  10705  wundm  10712  wunex2  10722  inar1  10759  ressxr  11252  nnssnn0  12506  un0addcl  12536  un0mulcl  12537  nn0ssxnn0  12579  hashbclem  14488  hashf1lem1  14491  hashf1lem2  14492  ccatrn  14626  trclublem  15031  relexpdmg  15078  relexpaddg  15089  fsumsplit  15791  fsum2d  15821  fsumabs  15852  fsumrlim  15862  fsumo1  15863  incexclem  15889  fprodsplit  16019  fprod2d  16034  lcmfunsnlem1  16694  coprmprod  16718  vdwapid1  17034  vdwlem6  17045  ramcl2  17075  isstruct2  17208  srngbase  17362  srngplusg  17363  srngmulr  17364  lmodbase  17378  lmodplusg  17379  lmodsca  17380  ipsbase  17389  ipsaddg  17390  ipsmulr  17391  phlbase  17399  phlplusg  17400  phlsca  17401  odrngbas  17456  odrngplusg  17457  odrngmulr  17458  prdssca  17508  prdsbas  17509  prdsplusg  17510  prdsmulr  17511  prdsvsca  17512  prdsip  17513  prdsle  17514  prdsds  17516  prdstset  17518  imasbas  17565  imasplusg  17570  imasmulr  17571  imassca  17572  imasvsca  17573  imasip  17574  mreexexlem2d  17700  drsdirfi  18360  ipobas  18586  ipotset  18588  acsfiindd  18608  psdmrn  18628  dirdm  18655  grpinvfval  19044  mulgfval  19134  gsumzsplit  19996  gsumsplit2  19998  gsumzunsnd  20025  gsum2dlem2  20040  dprdfadd  20091  dmdprdsplit2lem  20116  dmdprdsplit2  20117  dmdprdsplit  20118  dprdsplit  20119  ablfac1eulem  20143  gsumle  20214  lspun  21085  lspsolv  21244  lsppratlem3  21250  islbs3  21256  lbsextlem2  21260  lbsextlem4  21262  cnfldbas  21494  mpocnfldadd  21495  mpocnfldmul  21497  cnfldcj  21499  cnfldtset  21500  cnfldle  21501  cnfldds  21502  psrbas  22052  psrplusg  22055  psrmulr  22060  mplsubglem  22116  mplcoe1  22156  mplcoe5  22159  mdetunilem9  22745  basdif0  23078  ordtbas2  23316  ordtbas  23317  ordtopn1  23319  leordtval2  23337  iocpnfordt  23340  icomnfordt  23341  uncmp  23528  fiuncmp  23529  bwth  23535  locfincmp  23651  comppfsc  23657  1stckgenlem  23678  1stckgen  23679  ptbasin  23702  ptbasfi  23706  dfac14lem  23742  dfac14  23743  ptuncnv  23932  ptunhmeo  23933  ptcmpfi  23938  fbun  23965  trfil2  24012  ufprim  24034  ufileu  24044  filufint  24045  ufildr  24056  fmfnfm  24083  hausflim  24106  fclsfnflim  24152  alexsubALTlem4  24175  tmdgsum  24220  tsmsgsum  24264  tsmsres  24269  tsmssplit  24277  tsmsxplem1  24278  ustssco  24340  ustuqtop1  24366  prdsxmetlem  24493  prdsbl  24616  icccmplem2  24949  fsumcn  24997  cnmpopc  25055  rrxmetlem  25534  rrxmet  25535  rrxdstprj1  25536  ovolctb2  25619  ovolunnul  25627  ovolfiniun  25628  nulmbl2  25663  finiunmbl  25671  volfiniun  25674  icombl  25691  ioombl  25692  uniiccdif  25705  mbfres2  25772  itg2splitlem  25875  itg2split  25876  itgfsum  25954  itgsplit  25963  itgsplitioo  25965  dvreslem  26036  dvaddbr  26065  dvmulbr  26066  dvmptfsum  26102  lhop  26143  dvcnvrelem2  26145  mdegcl  26194  elplyr  26326  plyrem  26434  xrlimcnp  27098  fsumharmonic  27141  chtdif  27287  lgsdir2lem3  27456  lgsquadlem2  27510  dchrisum0lem1b  27644  pntrlog2bndlem6  27712  pntlemf  27734  nosupinfsep  27861  noetalem1  27870  cutsun12  27948  cofcutrtime  28085  addsuniflem  28159  addbday  28176  negsval  28183  mulsproplem12  28285  mulsproplem13  28286  mulsproplem14  28287  mulsuniflem  28307  mulsass  28324  precsexlem6  28370  precsexlem7  28371  precsexlem10  28374  precsexlem11  28375  ex-ss  30718  shsleji  31662  shsval2i  31679  ssjo  31739  sshhococi  31838  padct  33003  symgcom  33343  cycpmco2lem5  33390  cycpmco2lem6  33391  cycpmco2lem7  33392  cycpmco2  33393  gsumvsca1  33486  gsumvsca2  33487  elrgspnsubrunlem1  33507  rlocbas  33528  rlocaddval  33529  rlocmulval  33530  elrspunsn  33680  mxidlprm  33697  idlsrgbas  33738  idlsrgplusg  33739  idlsrgmulr  33741  fldextrspundgdvdslem  34014  fldextrspundgdvds  34015  constrextdg2lem  34082  esumsplit  34387  esumpad2  34390  aean  34578  sxbrsigalem2  34620  bnj931  35103  tz9.1regs  35469  subfacp1lem2b  35571  subfacp1lem3  35572  subfacp1lem5  35574  kur14lem7  35602  kur14lem9  35604  cvmliftlem10  35684  satfsschain  35754  fmlasssuc  35779  refssfne  36757  filnetlem3  36779  bj-unrab  37449  bj-snglsstag  37504  bj-2upln0  37546  bj-ccssccbar  37748  rdgssun  37911  finixpnum  38143  matunitlindflem1  38154  mbfresfi  38204  prdsbnd  38331  heibor1lem  38347  rrnequiv  38373  paddunssN  40471  sspadd1  40478  sspadd2  40479  pclfinN  40563  dochdmj1  42053  dvhdimlem  42107  elrfi  43316  mzpcompact2lem  43373  eldioph2  43384  eldioph4b  43429  ttac  43654  pwssplit4  43707  pwslnmlem2  43711  isnumbasgrplem2  43722  algbase  43792  algaddg  43793  algmulr  43794  fiuneneq  43810  idomsubgmo  43811  onexlimgt  43861  omabs2  43950  tfsconcatrnss12  43967  rclexi  44232  rtrclex  44234  trclubgNEW  44235  trclexi  44237  rtrclexi  44238  cnvrcl0  44242  cnvtrcl0  44243  dfrtrcl5  44246  trrelsuperrel2dg  44288  dfrcl2  44291  relexp0a  44333  relexpaddss  44335  trclimalb2  44343  frege83d  44365  frege131d  44381  dssmapnvod  44637  clsk3nimkb  44657  isotone1  44665  grumnudlem  44886  dmwf  45565  infxrpnf  46051  mccllem  46204  cncfiooicclem1  46498  dvmptfprod  46550  dvnprodlem1  46551  iblsplit  46571  fourierdlem54  46765  fourierdlem102  46813  fourierdlem103  46814  fourierdlem104  46815  fourierdlem114  46825  sge0resplit  47011  sge0split  47014  sge0splitmpt  47016  sge0xaddlem1  47038  isomenndlem  47135  hoiprodp1  47193  hoidmvlelem1  47200  hoidmvlelem2  47201  hoidmvlelem3  47202  hoidmvlelem4  47203  dfnbgrss2  48512  gsumsplit2f  48833  setrec1lem4  50352  elpglem2  50374