Theorem ssun1 4099

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

Syntax hints:   ∨ wo 844   ∈ wcel 2111   ∪ cun 3879   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898

This theorem is referenced by:  ssun2  4100  ssun3  4101  elun1  4103  difsssymdif  4179  inabs  4182  reuun1  4237  un00  4350  pwunss  4517  pwundif  4523  snsspr1  4707  snsstp1  4709  snsstp2  4710  uniintsn  4875  sofld  6011  sssucid  6236  fvrn0  6673  ovima0  7307  unexb  7451  dmexg  7594  suppun  7833  dftpos2  7892  tpostpos2  7896  wfrlem14  7951  wfrlem15  7952  tfrlem11  8007  oaabs2  8255  ralxpmap  8443  domss2  8660  mapunen  8670  ac6sfi  8746  frfi  8747  unfir  8770  domunfican  8775  iunfi  8796  elfiun  8878  dffi3  8879  unwdomg  9032  unxpwdom2  9036  unxpwdom  9037  cantnfp1lem1  9125  cantnfp1lem3  9127  tc2  9168  unwf  9223  rankunb  9263  r0weon  9423  infxpenlem  9424  dfac2b  9541  djudoml  9595  cdainflem  9598  infunabs  9618  infdju  9619  infdif  9620  ackbij1lem15  9645  cfsmolem  9681  isfin4p1  9726  fin23lem11  9728  fin1a2lem10  9820  fin1a2lem13  9823  axdc3lem4  9864  axcclem  9868  zornn0g  9916  ttukeylem1  9920  ttukeylem5  9924  ttukeylem7  9926  fingch  10034  fpwwe2lem13  10053  gchac  10092  wunfi  10132  wundm  10139  wunex2  10149  inar1  10186  ressxr  10674  nnssnn0  11888  un0addcl  11918  un0mulcl  11919  nn0ssxnn0  11958  hashbclem  13806  hashf1lem1  13809  hashf1lem2  13810  ccatrn  13934  trclublem  14346  relexpdmg  14393  relexpaddg  14404  fsumsplit  15089  fsum2d  15118  fsumabs  15148  fsumrlim  15158  fsumo1  15159  incexclem  15183  fprodsplit  15312  fprod2d  15327  lcmfunsnlem1  15971  coprmprod  15995  vdwapid1  16301  vdwlem6  16312  ramcl2  16342  isstruct2  16485  srngbase  16620  srngplusg  16621  srngmulr  16622  lmodbase  16629  lmodplusg  16630  lmodsca  16631  ipsbase  16636  ipsaddg  16637  ipsmulr  16638  phlbase  16646  phlplusg  16647  phlsca  16648  odrngbas  16672  odrngplusg  16673  odrngmulr  16674  prdssca  16721  prdsbas  16722  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  prdsip  16726  prdsle  16727  prdsds  16729  prdstset  16731  imasbas  16777  imasplusg  16782  imasmulr  16783  imassca  16784  imasvsca  16785  imasip  16786  mreexexlem2d  16908  drsdirfi  17540  ipobas  17757  ipotset  17759  acsfiindd  17779  psdmrn  17809  dirdm  17836  grpinvfval  18134  mulgfval  18218  gsumzsplit  19040  gsumsplit2  19042  gsumzunsnd  19069  gsum2dlem2  19084  dprdfadd  19135  dmdprdsplit2lem  19160  dmdprdsplit2  19161  dmdprdsplit  19162  dprdsplit  19163  ablfac1eulem  19187  lspun  19752  lspsolv  19908  lsppratlem3  19914  islbs3  19920  lbsextlem2  19924  lbsextlem4  19926  cnfldbas  20095  cnfldadd  20096  cnfldmul  20097  cnfldcj  20098  cnfldtset  20099  cnfldle  20100  cnfldds  20101  psrbagaddcl  20608  psrbas  20616  psrplusg  20619  psrmulr  20622  mplsubglem  20672  mplcoe1  20705  mplcoe5  20708  mdetunilem9  21225  basdif0  21558  ordtbas2  21796  ordtbas  21797  ordtopn1  21799  leordtval2  21817  iocpnfordt  21820  icomnfordt  21821  uncmp  22008  fiuncmp  22009  bwth  22015  locfincmp  22131  comppfsc  22137  1stckgenlem  22158  1stckgen  22159  ptbasin  22182  ptbasfi  22186  dfac14lem  22222  dfac14  22223  ptuncnv  22412  ptunhmeo  22413  ptcmpfi  22418  fbun  22445  trfil2  22492  ufprim  22514  ufileu  22524  filufint  22525  ufildr  22536  fmfnfm  22563  hausflim  22586  fclsfnflim  22632  alexsubALTlem4  22655  tmdgsum  22700  tsmsgsum  22744  tsmsres  22749  tsmssplit  22757  tsmsxplem1  22758  ustssco  22820  ustuqtop1  22847  prdsxmetlem  22975  prdsbl  23098  icccmplem2  23428  fsumcn  23475  cnmpopc  23533  rrxmetlem  24011  rrxmet  24012  rrxdstprj1  24013  ovolctb2  24096  ovolunnul  24104  ovolfiniun  24105  nulmbl2  24140  finiunmbl  24148  volfiniun  24151  icombl  24168  ioombl  24169  uniiccdif  24182  mbfres2  24249  itg2splitlem  24352  itg2split  24353  itgfsum  24430  itgsplit  24439  itgsplitioo  24441  dvreslem  24512  dvaddbr  24541  dvmulbr  24542  dvmptfsum  24578  lhop  24619  dvcnvrelem2  24621  mdegcl  24670  elplyr  24798  plyrem  24901  xrlimcnp  25554  fsumharmonic  25597  chtdif  25743  lgsdir2lem3  25911  lgsquadlem2  25965  dchrisum0lem1b  26099  pntrlog2bndlem6  26167  pntlemf  26189  ex-ss  28212  shsleji  29153  shsval2i  29170  ssjo  29230  sshhococi  29329  padct  30481  gsumle  30775  symgcom  30777  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmco2  30825  gsumvsca1  30904  gsumvsca2  30905  mxidlprm  31048  idlsrgbas  31057  idlsrgplusg  31058  idlsrgmulr  31060  esumsplit  31422  esumpad2  31425  aean  31613  sxbrsigalem2  31654  bnj931  32152  subfacp1lem2b  32541  subfacp1lem3  32542  subfacp1lem5  32544  kur14lem7  32572  kur14lem9  32574  cvmliftlem10  32654  satfsschain  32724  fmlasssuc  32749  dftrpred3g  33185  frrlem12  33247  frrlem13  33248  scutun12  33384  refssfne  33819  filnetlem3  33841  bj-unrab  34368  bj-snglsstag  34417  bj-2upln0  34459  bj-ccssccbar  34632  rdgssun  34795  finixpnum  35042  matunitlindflem1  35053  mbfresfi  35103  prdsbnd  35231  heibor1lem  35247  rrnequiv  35273  paddunssN  37104  sspadd1  37111  sspadd2  37112  pclfinN  37196  dochdmj1  38686  dvhdimlem  38740  elrfi  39635  mzpcompact2lem  39692  eldioph2  39703  eldioph4b  39752  ttac  39977  pwssplit4  40033  pwslnmlem2  40037  isnumbasgrplem2  40048  algbase  40122  algaddg  40123  algmulr  40124  fiuneneq  40141  idomsubgmo  40142  rclexi  40315  rtrclex  40317  trclubgNEW  40318  trclexi  40320  rtrclexi  40321  cnvrcl0  40325  cnvtrcl0  40326  dfrtrcl5  40329  trrelsuperrel2dg  40372  dfrcl2  40375  relexp0a  40417  relexpaddss  40419  trclimalb2  40427  frege83d  40449  frege131d  40465  dssmapnvod  40721  clsk3nimkb  40743  isotone1  40751  grumnudlem  40993  infxrpnf  42084  mccllem  42239  cncfiooicclem1  42535  dvmptfprod  42587  dvnprodlem1  42588  iblsplit  42608  fourierdlem54  42802  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem114  42862  sge0resplit  43045  sge0split  43048  sge0splitmpt  43050  sge0xaddlem1  43072  isomenndlem  43169  hoiprodp1  43227  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  gsumsplit2f  44440  setrec1lem4  45220  elpglem2  45241