Theorem ssun1 4124

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

This proof depends on syntax axioms:   ∨ wo 861   ∈ wcel 2145   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916

This theorem is used by:  ssun2  4125  ssun3  4126  elun1  4128  difsssymdif  4209  inabs  4212  reuun1  4274  un00  4357  pwunss  4575  pwundif  4582  snsspr1  4775  snsstp1  4777  snsstp2  4778  uniintsn  4945  sofld  6180  relresfld  6273  sssucid  6440  fvrn0  6907  f1ounsn  7274  ovima0  7594  unexb  7749  dmexg  7899  resf1extb  7932  xpord2indlem  8146  xpord3inddlem  8153  suppun  8183  dftpos2  8242  tpostpos2  8246  frrlem12  8297  frrlem13  8298  tfrlem11  8378  oaabs2  8638  ralxpmap  8904  domss2  9135  mapunen  9145  ac6sfi  9255  frfi  9256  unfir  9279  domunfican  9292  iunfi  9311  elfiun  9401  dffi3  9402  unwdomg  9557  unxpwdom2  9561  unxpwdom  9562  cantnfp1lem1  9658  cantnfp1lem3  9660  tc2  9720  unwf  9793  rankunb  9833  r0weon  10016  infxpenlem  10017  dfac2b  10134  djudoml  10188  cdainflem  10191  infunabs  10209  infdju  10210  infdif  10211  ackbij1lem15  10236  cfsmolem  10273  isfin4p1  10318  fin23lem11  10320  fin1a2lem10  10412  fin1a2lem13  10415  axdc3lem4  10456  axcclem  10460  zornn0g  10508  ttukeylem1  10512  ttukeylem5  10516  ttukeylem7  10518  fingch  10633  fpwwe2lem12  10652  gchac  10691  wunfi  10731  wundm  10738  wunex2  10748  inar1  10785  ressxr  11278  nnssnn0  12532  un0addcl  12562  un0mulcl  12563  nn0ssxnn0  12605  hashbclem  14518  hashf1lem1  14521  hashf1lem2  14522  ccatrn  14656  trclublem  15069  relexpdmg  15116  relexpaddg  15127  fsumsplit  15828  fsum2d  15858  fsumabs  15889  fsumrlim  15899  fsumo1  15900  incexclem  15926  fprodsplit  16054  fprod2d  16069  lcmfunsnlem1  16728  coprmprod  16752  vdwapid1  17068  vdwlem6  17079  ramcl2  17109  isstruct2  17242  srngbase  17396  srngplusg  17397  srngmulr  17398  lmodbase  17412  lmodplusg  17413  lmodsca  17414  ipsbase  17423  ipsaddg  17424  ipsmulr  17425  phlbase  17433  phlplusg  17434  phlsca  17435  odrngbas  17490  odrngplusg  17491  odrngmulr  17492  prdssca  17542  prdsbas  17543  prdsplusg  17544  prdsmulr  17545  prdsvsca  17546  prdsip  17547  prdsle  17548  prdsds  17550  prdstset  17552  imasbas  17599  imasplusg  17604  imasmulr  17605  imassca  17606  imasvsca  17607  imasip  17608  mreexexlem2d  17734  drsdirfi  18394  ipobas  18620  ipotset  18622  acsfiindd  18642  psdmrn  18662  dirdm  18689  grpinvfval  19103  mulgfval  19193  gsumzsplit  20055  gsumsplit2  20057  gsumzunsnd  20084  gsum2dlem2  20099  dprdfadd  20150  dmdprdsplit2lem  20175  dmdprdsplit2  20176  dmdprdsplit  20177  dprdsplit  20178  ablfac1eulem  20202  gsumle  20273  lspun  21172  lspsolv  21331  lsppratlem3  21337  islbs3  21343  lbsextlem2  21347  lbsextlem4  21349  cnfldbas  21590  mpocnfldadd  21591  mpocnfldmul  21593  cnfldcj  21595  cnfldtset  21596  cnfldle  21597  cnfldds  21598  psrbas  22150  psrplusg  22153  psrmulr  22158  mplsubglem  22214  mplcoe1  22254  mplcoe5  22257  mdetunilem9  22843  matunitlindflem1  22902  basdif0  23179  ordtbas2  23417  ordtbas  23418  ordtopn1  23420  leordtval2  23438  iocpnfordt  23441  icomnfordt  23442  uncmp  23629  fiuncmp  23630  bwth  23636  locfincmp  23753  comppfsc  23759  1stckgenlem  23780  1stckgen  23781  ptbasin  23804  ptbasfi  23808  dfac14lem  23844  dfac14  23845  ptuncnv  24034  ptunhmeo  24035  ptcmpfi  24040  fbun  24067  trfil2  24114  ufprim  24136  ufileu  24146  filufint  24147  ufildr  24158  fmfnfm  24185  hausflim  24208  fclsfnflim  24254  alexsubALTlem4  24277  tmdgsum  24322  tsmsgsum  24366  tsmsres  24371  tsmssplit  24379  tsmsxplem1  24380  ustssco  24442  ustuqtop1  24468  prdsxmetlem  24595  prdsbl  24718  icccmplem2  25051  fsumcn  25099  cnmpopc  25157  rrxmetlem  25636  rrxmet  25637  rrxdstprj1  25638  ovolctb2  25721  ovolunnul  25729  ovolfiniun  25730  nulmbl2  25765  finiunmbl  25773  volfiniun  25776  icombl  25793  ioombl  25794  uniiccdif  25807  mbfres2  25874  itg2splitlem  25977  itg2split  25978  itgfsum  26055  itgsplit  26064  itgsplitioo  26066  dvreslem  26137  dvaddbr  26166  dvmulbr  26167  dvmptfsum  26203  lhop  26244  dvcnvrelem2  26246  mdegcl  26295  elplyr  26427  plyrem  26536  xrlimcnp  27206  fsumharmonic  27249  chtdif  27395  lgsdir2lem3  27564  lgsquadlem2  27618  dchrisum0lem1b  27752  pntrlog2bndlem6  27820  pntlemf  27842  nosupinfsep  27969  noetalem1  27978  cutsun12  28056  cofcutrtime  28193  addsuniflem  28267  addbday  28284  negsval  28291  mulsproplem12  28393  mulsproplem13  28394  mulsproplem14  28395  mulsuniflem  28415  mulsass  28432  precsexlem6  28478  precsexlem7  28479  precsexlem10  28482  precsexlem11  28483  ex-ss  30908  shsleji  31852  shsval2i  31869  ssjo  31929  sshhococi  32028  padct  33190  symgcom  33524  cycpmco2lem5  33571  cycpmco2lem6  33572  cycpmco2lem7  33573  cycpmco2  33574  gsumvsca1  33667  gsumvsca2  33668  elrgspnsubrunlem1  33688  rlocbas  33709  rlocaddval  33710  rlocmulval  33711  elrspunsn  33858  mxidlprm  33874  idlsrgbas  33915  idlsrgplusg  33916  idlsrgmulr  33918  fldextrspundgdvdslem  34191  fldextrspundgdvds  34192  constrextdg2lem  34259  esumsplit  34564  esumpad2  34567  aean  34756  sxbrsigalem2  34798  bnj931  35281  tz9.1regs  35661  subfacp1lem2b  35761  subfacp1lem3  35762  subfacp1lem5  35764  kur14lem7  35792  kur14lem9  35794  cvmliftlem10  35874  satfsschain  35944  fmlasssuc  35969  refssfne  36978  filnetlem3  37000  bj-unrab  37671  bj-snglsstag  37726  bj-2upln0  37768  bj-ccssccbar  37970  rdgssun  38133  finixpnum  38360  mbfresfi  38416  prdsbnd  38544  heibor1lem  38560  rrnequiv  38586  paddunssN  40682  sspadd1  40689  sspadd2  40690  pclfinN  40774  dochdmj1  42264  dvhdimlem  42318  elrfi  43540  mzpcompact2lem  43597  eldioph2  43608  eldioph4b  43653  ttac  43878  pwssplit4  43931  pwslnmlem2  43935  isnumbasgrplem2  43946  algbase  44016  algaddg  44017  algmulr  44018  fiuneneq  44034  idomsubgmo  44035  onexlimgt  44085  omabs2  44174  tfsconcatrnss12  44191  rclexi  44456  rtrclex  44458  trclubgNEW  44459  trclexi  44461  rtrclexi  44462  cnvrcl0  44466  cnvtrcl0  44467  dfrtrcl5  44470  trrelsuperrel2dg  44512  dfrcl2  44515  relexp0a  44557  relexpaddss  44559  trclimalb2  44567  frege83d  44589  frege131d  44605  dssmapnvod  44861  clsk3nimkb  44881  isotone1  44889  grumnudlem  45110  dmwf  45789  infxrpnf  46275  mccllem  46428  cncfiooicclem1  46722  dvmptfprod  46774  dvnprodlem1  46775  iblsplit  46795  fourierdlem54  46989  fourierdlem102  47037  fourierdlem103  47038  fourierdlem104  47039  fourierdlem114  47049  sge0resplit  47235  sge0split  47238  sge0splitmpt  47240  sge0xaddlem1  47262  isomenndlem  47359  hoiprodp1  47417  hoidmvlelem1  47424  hoidmvlelem2  47425  hoidmvlelem3  47426  hoidmvlelem4  47427  wrddun  47718  chndun  47723  chnrun  47728  dfnbgrss2  48776  gsumsplit2f  49096  setrec1lem4  50617  elpglem2  50639