Theorem ssun1 4107

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 873	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 4083	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 235	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3919	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 853   ∈ wcel 2119   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900

This theorem is referenced by:  ssun2  4108  ssun3  4109  elun1  4111  difsssymdif  4191  inabs  4194  reuun1  4256  un00  4373  pwunss  4547  pwundif  4553  snsspr1  4745  snsstp1  4747  snsstp2  4748  uniintsn  4915  sofld  6138  sssucid  6392  fvrn0  6855  f1ounsn  7216  ovima0  7535  unexb  7690  unexbOLD  7691  dmexg  7841  resf1extb  7874  xpord2indlem  8087  xpord3inddlem  8094  suppun  8124  dftpos2  8183  tpostpos2  8187  frrlem12  8237  frrlem13  8238  tfrlem11  8317  oaabs2  8575  ralxpmap  8834  domss2  9064  mapunen  9074  ac6sfi  9184  frfi  9185  unfir  9208  domunfican  9222  iunfi  9243  elfiun  9333  dffi3  9334  unwdomg  9489  unxpwdom2  9493  unxpwdom  9494  cantnfp1lem1  9590  cantnfp1lem3  9592  tc2  9652  unwf  9725  rankunb  9765  r0weon  9925  infxpenlem  9926  dfac2b  10044  djudoml  10098  cdainflem  10101  infunabs  10119  infdju  10120  infdif  10121  ackbij1lem15  10146  cfsmolem  10183  isfin4p1  10228  fin23lem11  10230  fin1a2lem10  10322  fin1a2lem13  10325  axdc3lem4  10366  axcclem  10370  zornn0g  10418  ttukeylem1  10422  ttukeylem5  10426  ttukeylem7  10428  fingch  10537  fpwwe2lem12  10556  gchac  10595  wunfi  10635  wundm  10642  wunex2  10652  inar1  10689  ressxr  11180  nnssnn0  12431  un0addcl  12461  un0mulcl  12462  nn0ssxnn0  12504  hashbclem  14405  hashf1lem1  14408  hashf1lem2  14409  ccatrn  14543  trclublem  14948  relexpdmg  14995  relexpaddg  15006  fsumsplit  15694  fsum2d  15724  fsumabs  15755  fsumrlim  15765  fsumo1  15766  incexclem  15792  fprodsplit  15922  fprod2d  15937  lcmfunsnlem1  16597  coprmprod  16621  vdwapid1  16937  vdwlem6  16948  ramcl2  16978  isstruct2  17110  srngbase  17264  srngplusg  17265  srngmulr  17266  lmodbase  17280  lmodplusg  17281  lmodsca  17282  ipsbase  17291  ipsaddg  17292  ipsmulr  17293  phlbase  17301  phlplusg  17302  phlsca  17303  odrngbas  17358  odrngplusg  17359  odrngmulr  17360  prdssca  17410  prdsbas  17411  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  prdsip  17415  prdsle  17416  prdsds  17418  prdstset  17420  imasbas  17467  imasplusg  17472  imasmulr  17473  imassca  17474  imasvsca  17475  imasip  17476  mreexexlem2d  17602  drsdirfi  18262  ipobas  18488  ipotset  18490  acsfiindd  18510  psdmrn  18530  dirdm  18557  grpinvfval  18945  mulgfval  19036  gsumzsplit  19893  gsumsplit2  19895  gsumzunsnd  19922  gsum2dlem2  19937  dprdfadd  19988  dmdprdsplit2lem  20013  dmdprdsplit2  20014  dmdprdsplit  20015  dprdsplit  20016  ablfac1eulem  20040  gsumle  20111  lspun  20977  lspsolv  21136  lsppratlem3  21142  islbs3  21148  lbsextlem2  21152  lbsextlem4  21154  cnfldbas  21351  mpocnfldadd  21352  mpocnfldmul  21354  cnfldcj  21356  cnfldtset  21357  cnfldle  21358  cnfldds  21359  psrbas  21909  psrplusg  21912  psrmulr  21917  mplsubglem  21973  mplcoe1  22013  mplcoe5  22016  mdetunilem9  22603  basdif0  22936  ordtbas2  23174  ordtbas  23175  ordtopn1  23177  leordtval2  23195  iocpnfordt  23198  icomnfordt  23199  uncmp  23386  fiuncmp  23387  bwth  23393  locfincmp  23509  comppfsc  23515  1stckgenlem  23536  1stckgen  23537  ptbasin  23560  ptbasfi  23564  dfac14lem  23600  dfac14  23601  ptuncnv  23790  ptunhmeo  23791  ptcmpfi  23796  fbun  23823  trfil2  23870  ufprim  23892  ufileu  23902  filufint  23903  ufildr  23914  fmfnfm  23941  hausflim  23964  fclsfnflim  24010  alexsubALTlem4  24033  tmdgsum  24078  tsmsgsum  24122  tsmsres  24127  tsmssplit  24135  tsmsxplem1  24136  ustssco  24198  ustuqtop1  24224  prdsxmetlem  24351  prdsbl  24474  icccmplem2  24807  fsumcn  24855  cnmpopc  24913  rrxmetlem  25392  rrxmet  25393  rrxdstprj1  25394  ovolctb2  25477  ovolunnul  25485  ovolfiniun  25486  nulmbl2  25521  finiunmbl  25529  volfiniun  25532  icombl  25549  ioombl  25550  uniiccdif  25563  mbfres2  25630  itg2splitlem  25733  itg2split  25734  itgfsum  25812  itgsplit  25821  itgsplitioo  25823  dvreslem  25894  dvaddbr  25923  dvmulbr  25924  dvmptfsum  25960  lhop  26001  dvcnvrelem2  26003  mdegcl  26052  elplyr  26184  plyrem  26289  xrlimcnp  26950  fsumharmonic  26993  chtdif  27139  lgsdir2lem3  27308  lgsquadlem2  27362  dchrisum0lem1b  27496  pntrlog2bndlem6  27564  pntlemf  27586  nosupinfsep  27714  noetalem1  27723  cutsun12  27800  cofcutrtime  27937  addsuniflem  28011  addbday  28028  negsval  28035  mulsproplem12  28137  mulsproplem13  28138  mulsproplem14  28139  mulsuniflem  28159  mulsass  28176  precsexlem6  28222  precsexlem7  28223  precsexlem10  28226  precsexlem11  28227  ex-ss  30515  shsleji  31459  shsval2i  31476  ssjo  31536  sshhococi  31635  padct  32810  symgcom  33164  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2lem7  33213  cycpmco2  33214  gsumvsca1  33307  gsumvsca2  33308  elrgspnsubrunlem1  33328  rlocbas  33348  rlocaddval  33349  rlocmulval  33350  elrspunsn  33512  mxidlprm  33553  idlsrgbas  33587  idlsrgplusg  33588  idlsrgmulr  33590  fldextrspundgdvdslem  33864  fldextrspundgdvds  33865  constrextdg2lem  33932  esumsplit  34237  esumpad2  34240  aean  34428  sxbrsigalem2  34470  bnj931  34953  tz9.1regs  35315  subfacp1lem2b  35409  subfacp1lem3  35410  subfacp1lem5  35412  kur14lem7  35440  kur14lem9  35442  cvmliftlem10  35522  satfsschain  35592  fmlasssuc  35617  refssfne  36586  filnetlem3  36608  bj-unrab  37279  bj-snglsstag  37334  bj-2upln0  37376  bj-ccssccbar  37577  rdgssun  37740  finixpnum  37972  matunitlindflem1  37983  mbfresfi  38033  prdsbnd  38160  heibor1lem  38176  rrnequiv  38202  paddunssN  40300  sspadd1  40307  sspadd2  40308  pclfinN  40392  dochdmj1  41882  dvhdimlem  41936  elrfi  43143  mzpcompact2lem  43200  eldioph2  43211  eldioph4b  43256  ttac  43481  pwssplit4  43534  pwslnmlem2  43538  isnumbasgrplem2  43549  algbase  43619  algaddg  43620  algmulr  43621  fiuneneq  43637  idomsubgmo  43638  onexlimgt  43688  omabs2  43777  tfsconcatrnss12  43794  rclexi  44059  rtrclex  44061  trclubgNEW  44062  trclexi  44064  rtrclexi  44065  cnvrcl0  44069  cnvtrcl0  44070  dfrtrcl5  44073  trrelsuperrel2dg  44115  dfrcl2  44118  relexp0a  44160  relexpaddss  44162  trclimalb2  44170  frege83d  44192  frege131d  44208  dssmapnvod  44464  clsk3nimkb  44484  isotone1  44492  grumnudlem  44729  dmwf  45409  infxrpnf  45889  mccllem  46042  cncfiooicclem1  46336  dvmptfprod  46388  dvnprodlem1  46389  iblsplit  46409  fourierdlem54  46603  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  sge0resplit  46849  sge0split  46852  sge0splitmpt  46854  sge0xaddlem1  46876  isomenndlem  46973  hoiprodp1  47031  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  dfnbgrss2  48350  gsumsplit2f  48671  setrec1lem4  50180  elpglem2  50202