Theorem ssun1 4160

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

Syntax hints:   ∨ wo 847   ∈ wcel 2107   ∪ cun 3931   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-un 3938  df-ss 3950

This theorem is referenced by:  ssun2  4161  ssun3  4162  elun1  4164  difsssymdif  4245  inabs  4248  reuun1  4310  un00  4427  pwunss  4600  pwundif  4606  snsspr1  4796  snsstp1  4798  snsstp2  4799  uniintsn  4967  sofld  6189  sssucid  6445  fvrn0  6917  f1ounsn  7275  ovima0  7595  unexb  7750  unexbOLD  7751  dmexg  7906  resf1extb  7939  xpord2indlem  8155  xpord3inddlem  8162  suppun  8192  dftpos2  8251  tpostpos2  8255  frrlem12  8305  frrlem13  8306  wfrlem14OLD  8345  wfrlem15OLD  8346  tfrlem11  8411  oaabs2  8670  ralxpmap  8919  domss2  9159  mapunen  9169  ac6sfi  9303  frfi  9304  unfir  9329  domunfican  9344  iunfi  9366  elfiun  9453  dffi3  9454  unwdomg  9607  unxpwdom2  9611  unxpwdom  9612  cantnfp1lem1  9701  cantnfp1lem3  9703  tc2  9765  unwf  9833  rankunb  9873  r0weon  10035  infxpenlem  10036  dfac2b  10154  djudoml  10208  cdainflem  10211  infunabs  10229  infdju  10230  infdif  10231  ackbij1lem15  10256  cfsmolem  10293  isfin4p1  10338  fin23lem11  10340  fin1a2lem10  10432  fin1a2lem13  10435  axdc3lem4  10476  axcclem  10480  zornn0g  10528  ttukeylem1  10532  ttukeylem5  10536  ttukeylem7  10538  fingch  10646  fpwwe2lem12  10665  gchac  10704  wunfi  10744  wundm  10751  wunex2  10761  inar1  10798  ressxr  11288  nnssnn0  12513  un0addcl  12543  un0mulcl  12544  nn0ssxnn0  12586  hashbclem  14474  hashf1lem1  14477  hashf1lem2  14478  ccatrn  14610  trclublem  15017  relexpdmg  15064  relexpaddg  15075  fsumsplit  15760  fsum2d  15790  fsumabs  15820  fsumrlim  15830  fsumo1  15831  incexclem  15855  fprodsplit  15985  fprod2d  16000  lcmfunsnlem1  16657  coprmprod  16681  vdwapid1  16996  vdwlem6  17007  ramcl2  17037  isstruct2  17169  srngbase  17331  srngplusg  17332  srngmulr  17333  lmodbase  17347  lmodplusg  17348  lmodsca  17349  ipsbase  17358  ipsaddg  17359  ipsmulr  17360  phlbase  17368  phlplusg  17369  phlsca  17370  odrngbas  17425  odrngplusg  17426  odrngmulr  17427  prdssca  17477  prdsbas  17478  prdsplusg  17479  prdsmulr  17480  prdsvsca  17481  prdsip  17482  prdsle  17483  prdsds  17485  prdstset  17487  imasbas  17533  imasplusg  17538  imasmulr  17539  imassca  17540  imasvsca  17541  imasip  17542  mreexexlem2d  17664  drsdirfi  18326  ipobas  18550  ipotset  18552  acsfiindd  18572  psdmrn  18592  dirdm  18619  grpinvfval  18970  mulgfval  19061  gsumzsplit  19918  gsumsplit2  19920  gsumzunsnd  19947  gsum2dlem2  19962  dprdfadd  20013  dmdprdsplit2lem  20038  dmdprdsplit2  20039  dmdprdsplit  20040  dprdsplit  20041  ablfac1eulem  20065  lspun  20958  lspsolv  21118  lsppratlem3  21124  islbs3  21130  lbsextlem2  21134  lbsextlem4  21136  cnfldbas  21335  mpocnfldadd  21336  mpocnfldmul  21338  cnfldcj  21340  cnfldtset  21341  cnfldle  21342  cnfldds  21343  cnfldbasOLD  21350  cnfldaddOLD  21351  cnfldmulOLD  21352  cnfldcjOLD  21353  cnfldtsetOLD  21354  cnfldleOLD  21355  cnflddsOLD  21356  psrbas  21920  psrplusg  21923  psrmulr  21929  mplsubglem  21986  mplcoe1  22022  mplcoe5  22025  mdetunilem9  22593  basdif0  22926  ordtbas2  23164  ordtbas  23165  ordtopn1  23167  leordtval2  23185  iocpnfordt  23188  icomnfordt  23189  uncmp  23376  fiuncmp  23377  bwth  23383  locfincmp  23499  comppfsc  23505  1stckgenlem  23526  1stckgen  23527  ptbasin  23550  ptbasfi  23554  dfac14lem  23590  dfac14  23591  ptuncnv  23780  ptunhmeo  23781  ptcmpfi  23786  fbun  23813  trfil2  23860  ufprim  23882  ufileu  23892  filufint  23893  ufildr  23904  fmfnfm  23931  hausflim  23954  fclsfnflim  24000  alexsubALTlem4  24023  tmdgsum  24068  tsmsgsum  24112  tsmsres  24117  tsmssplit  24125  tsmsxplem1  24126  ustssco  24188  ustuqtop1  24215  prdsxmetlem  24342  prdsbl  24467  icccmplem2  24800  fsumcn  24849  cnmpopc  24910  rrxmetlem  25396  rrxmet  25397  rrxdstprj1  25398  ovolctb2  25482  ovolunnul  25490  ovolfiniun  25491  nulmbl2  25526  finiunmbl  25534  volfiniun  25537  icombl  25554  ioombl  25555  uniiccdif  25568  mbfres2  25635  itg2splitlem  25738  itg2split  25739  itgfsum  25817  itgsplit  25826  itgsplitioo  25828  dvreslem  25899  dvaddbr  25929  dvmulbr  25930  dvmulbrOLD  25931  dvmptfsum  25968  lhop  26010  dvcnvrelem2  26012  mdegcl  26063  elplyr  26195  plyrem  26302  xrlimcnp  26966  fsumharmonic  27010  chtdif  27156  lgsdir2lem3  27326  lgsquadlem2  27380  dchrisum0lem1b  27514  pntrlog2bndlem6  27582  pntlemf  27604  nosupinfsep  27732  noetalem1  27741  scutun12  27810  cofcutrtime  27916  addsuniflem  27989  addsbday  28005  negsval  28012  mulsproplem12  28108  mulsproplem13  28109  mulsproplem14  28110  mulsuniflem  28130  mulsass  28147  precsexlem6  28191  precsexlem7  28192  precsexlem10  28195  precsexlem11  28196  ex-ss  30393  shsleji  31336  shsval2i  31353  ssjo  31413  sshhococi  31512  padct  32678  gsumle  33047  symgcom  33049  cycpmco2lem5  33096  cycpmco2lem6  33097  cycpmco2lem7  33098  cycpmco2  33099  gsumvsca1  33178  gsumvsca2  33179  elrgspnsubrunlem1  33197  rlocbas  33217  rlocaddval  33218  rlocmulval  33219  elrspunsn  33398  mxidlprm  33439  idlsrgbas  33473  idlsrgplusg  33474  idlsrgmulr  33476  fldextrspundgdvdslem  33671  fldextrspundgdvds  33672  constrextdg2lem  33730  esumsplit  33995  esumpad2  33998  aean  34186  sxbrsigalem2  34229  bnj931  34725  subfacp1lem2b  35127  subfacp1lem3  35128  subfacp1lem5  35130  kur14lem7  35158  kur14lem9  35160  cvmliftlem10  35240  satfsschain  35310  fmlasssuc  35335  refssfne  36300  filnetlem3  36322  bj-unrab  36868  bj-snglsstag  36923  bj-2upln0  36965  bj-ccssccbar  37159  rdgssun  37320  finixpnum  37553  matunitlindflem1  37564  mbfresfi  37614  prdsbnd  37741  heibor1lem  37757  rrnequiv  37783  paddunssN  39751  sspadd1  39758  sspadd2  39759  pclfinN  39843  dochdmj1  41333  dvhdimlem  41387  elrfi  42650  mzpcompact2lem  42707  eldioph2  42718  eldioph4b  42767  ttac  42993  pwssplit4  43046  pwslnmlem2  43050  isnumbasgrplem2  43061  algbase  43131  algaddg  43132  algmulr  43133  fiuneneq  43149  idomsubgmo  43150  onexlimgt  43200  omabs2  43290  tfsconcatrnss12  43307  rclexi  43573  rtrclex  43575  trclubgNEW  43576  trclexi  43578  rtrclexi  43579  cnvrcl0  43583  cnvtrcl0  43584  dfrtrcl5  43587  trrelsuperrel2dg  43629  dfrcl2  43632  relexp0a  43674  relexpaddss  43676  trclimalb2  43684  frege83d  43706  frege131d  43722  dssmapnvod  43978  clsk3nimkb  43998  isotone1  44006  grumnudlem  44249  dmwf  44927  infxrpnf  45402  mccllem  45557  cncfiooicclem1  45853  dvmptfprod  45905  dvnprodlem1  45906  iblsplit  45926  fourierdlem54  46120  fourierdlem102  46168  fourierdlem103  46169  fourierdlem104  46170  fourierdlem114  46180  sge0resplit  46366  sge0split  46369  sge0splitmpt  46371  sge0xaddlem1  46393  isomenndlem  46490  hoiprodp1  46548  hoidmvlelem1  46555  hoidmvlelem2  46556  hoidmvlelem3  46557  hoidmvlelem4  46558  dfnbgrss2  47791  gsumsplit2f  48042  setrec1lem4  49205  elpglem2  49227