Theorem ssun1 4130

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 878	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 4106	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 236	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3940	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 858   ∈ wcel 2142   ∪ cun 3902   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921

This theorem is referenced by:  ssun2  4131  ssun3  4132  elun1  4134  difsssymdif  4215  inabs  4218  reuun1  4280  un00  4399  pwunss  4573  pwundif  4580  snsspr1  4772  snsstp1  4774  snsstp2  4775  uniintsn  4943  sofld  6173  sssucid  6428  fvrn0  6895  f1ounsn  7256  ovima0  7575  unexb  7730  unexbOLD  7731  dmexg  7882  resf1extb  7915  xpord2indlem  8127  xpord3inddlem  8134  suppun  8164  dftpos2  8223  tpostpos2  8227  frrlem12  8278  frrlem13  8279  tfrlem11  8359  oaabs2  8619  ralxpmap  8878  domss2  9108  mapunen  9118  ac6sfi  9228  frfi  9229  unfir  9252  domunfican  9266  iunfi  9286  elfiun  9376  dffi3  9377  unwdomg  9532  unxpwdom2  9536  unxpwdom  9537  cantnfp1lem1  9633  cantnfp1lem3  9635  tc2  9695  unwf  9768  rankunb  9808  r0weon  9968  infxpenlem  9969  dfac2b  10087  djudoml  10141  cdainflem  10144  infunabs  10162  infdju  10163  infdif  10164  ackbij1lem15  10189  cfsmolem  10227  isfin4p1  10272  fin23lem11  10274  fin1a2lem10  10366  fin1a2lem13  10369  axdc3lem4  10410  axcclem  10414  zornn0g  10462  ttukeylem1  10466  ttukeylem5  10470  ttukeylem7  10472  fingch  10581  fpwwe2lem12  10600  gchac  10639  wunfi  10679  wundm  10686  wunex2  10696  inar1  10733  ressxr  11226  nnssnn0  12484  un0addcl  12514  un0mulcl  12515  nn0ssxnn0  12557  hashbclem  14465  hashf1lem1  14468  hashf1lem2  14469  ccatrn  14603  trclublem  15008  relexpdmg  15055  relexpaddg  15066  fsumsplit  15768  fsum2d  15798  fsumabs  15829  fsumrlim  15839  fsumo1  15840  incexclem  15866  fprodsplit  15996  fprod2d  16011  lcmfunsnlem1  16671  coprmprod  16695  vdwapid1  17011  vdwlem6  17022  ramcl2  17052  isstruct2  17185  srngbase  17339  srngplusg  17340  srngmulr  17341  lmodbase  17355  lmodplusg  17356  lmodsca  17357  ipsbase  17366  ipsaddg  17367  ipsmulr  17368  phlbase  17376  phlplusg  17377  phlsca  17378  odrngbas  17433  odrngplusg  17434  odrngmulr  17435  prdssca  17485  prdsbas  17486  prdsplusg  17487  prdsmulr  17488  prdsvsca  17489  prdsip  17490  prdsle  17491  prdsds  17493  prdstset  17495  imasbas  17542  imasplusg  17547  imasmulr  17548  imassca  17549  imasvsca  17550  imasip  17551  mreexexlem2d  17677  drsdirfi  18337  ipobas  18563  ipotset  18565  acsfiindd  18585  psdmrn  18605  dirdm  18632  grpinvfval  19020  mulgfval  19111  gsumzsplit  19967  gsumsplit2  19969  gsumzunsnd  19996  gsum2dlem2  20011  dprdfadd  20062  dmdprdsplit2lem  20087  dmdprdsplit2  20088  dmdprdsplit  20089  dprdsplit  20090  ablfac1eulem  20114  gsumle  20185  lspun  21051  lspsolv  21210  lsppratlem3  21216  islbs3  21222  lbsextlem2  21226  lbsextlem4  21228  cnfldbas  21425  mpocnfldadd  21426  mpocnfldmul  21428  cnfldcj  21430  cnfldtset  21431  cnfldle  21432  cnfldds  21433  psrbas  21983  psrplusg  21986  psrmulr  21991  mplsubglem  22047  mplcoe1  22087  mplcoe5  22090  mdetunilem9  22677  basdif0  23010  ordtbas2  23248  ordtbas  23249  ordtopn1  23251  leordtval2  23269  iocpnfordt  23272  icomnfordt  23273  uncmp  23460  fiuncmp  23461  bwth  23467  locfincmp  23583  comppfsc  23589  1stckgenlem  23610  1stckgen  23611  ptbasin  23634  ptbasfi  23638  dfac14lem  23674  dfac14  23675  ptuncnv  23864  ptunhmeo  23865  ptcmpfi  23870  fbun  23897  trfil2  23944  ufprim  23966  ufileu  23976  filufint  23977  ufildr  23988  fmfnfm  24015  hausflim  24038  fclsfnflim  24084  alexsubALTlem4  24107  tmdgsum  24152  tsmsgsum  24196  tsmsres  24201  tsmssplit  24209  tsmsxplem1  24210  ustssco  24272  ustuqtop1  24298  prdsxmetlem  24425  prdsbl  24548  icccmplem2  24881  fsumcn  24929  cnmpopc  24987  rrxmetlem  25466  rrxmet  25467  rrxdstprj1  25468  ovolctb2  25551  ovolunnul  25559  ovolfiniun  25560  nulmbl2  25595  finiunmbl  25603  volfiniun  25606  icombl  25623  ioombl  25624  uniiccdif  25637  mbfres2  25704  itg2splitlem  25807  itg2split  25808  itgfsum  25886  itgsplit  25895  itgsplitioo  25897  dvreslem  25968  dvaddbr  25997  dvmulbr  25998  dvmptfsum  26034  lhop  26075  dvcnvrelem2  26077  mdegcl  26126  elplyr  26258  plyrem  26366  xrlimcnp  27030  fsumharmonic  27073  chtdif  27219  lgsdir2lem3  27388  lgsquadlem2  27442  dchrisum0lem1b  27576  pntrlog2bndlem6  27644  pntlemf  27666  nosupinfsep  27793  noetalem1  27802  cutsun12  27880  cofcutrtime  28017  addsuniflem  28091  addbday  28108  negsval  28115  mulsproplem12  28217  mulsproplem13  28218  mulsproplem14  28219  mulsuniflem  28239  mulsass  28256  precsexlem6  28302  precsexlem7  28303  precsexlem10  28306  precsexlem11  28307  ex-ss  30626  shsleji  31570  shsval2i  31587  ssjo  31647  sshhococi  31746  padct  32917  symgcom  33260  cycpmco2lem5  33307  cycpmco2lem6  33308  cycpmco2lem7  33309  cycpmco2  33310  gsumvsca1  33403  gsumvsca2  33404  elrgspnsubrunlem1  33425  rlocbas  33446  rlocaddval  33447  rlocmulval  33448  elrspunsn  33612  mxidlprm  33655  idlsrgbas  33697  idlsrgplusg  33698  idlsrgmulr  33700  fldextrspundgdvdslem  33974  fldextrspundgdvds  33975  constrextdg2lem  34042  esumsplit  34347  esumpad2  34350  aean  34538  sxbrsigalem2  34580  bnj931  35063  tz9.1regs  35427  subfacp1lem2b  35528  subfacp1lem3  35529  subfacp1lem5  35531  kur14lem7  35559  kur14lem9  35561  cvmliftlem10  35641  satfsschain  35711  fmlasssuc  35736  refssfne  36715  filnetlem3  36737  bj-unrab  37408  bj-snglsstag  37463  bj-2upln0  37505  bj-ccssccbar  37706  rdgssun  37869  finixpnum  38101  matunitlindflem1  38112  mbfresfi  38162  prdsbnd  38289  heibor1lem  38305  rrnequiv  38331  paddunssN  40429  sspadd1  40436  sspadd2  40437  pclfinN  40521  dochdmj1  42011  dvhdimlem  42065  elrfi  43272  mzpcompact2lem  43329  eldioph2  43340  eldioph4b  43385  ttac  43610  pwssplit4  43663  pwslnmlem2  43667  isnumbasgrplem2  43678  algbase  43748  algaddg  43749  algmulr  43750  fiuneneq  43766  idomsubgmo  43767  onexlimgt  43817  omabs2  43906  tfsconcatrnss12  43923  rclexi  44188  rtrclex  44190  trclubgNEW  44191  trclexi  44193  rtrclexi  44194  cnvrcl0  44198  cnvtrcl0  44199  dfrtrcl5  44202  trrelsuperrel2dg  44244  dfrcl2  44247  relexp0a  44289  relexpaddss  44291  trclimalb2  44299  frege83d  44321  frege131d  44337  dssmapnvod  44593  clsk3nimkb  44613  isotone1  44621  grumnudlem  44858  dmwf  45538  infxrpnf  46017  mccllem  46170  cncfiooicclem1  46464  dvmptfprod  46516  dvnprodlem1  46517  iblsplit  46537  fourierdlem54  46731  fourierdlem102  46779  fourierdlem103  46780  fourierdlem104  46781  fourierdlem114  46791  sge0resplit  46977  sge0split  46980  sge0splitmpt  46982  sge0xaddlem1  47004  isomenndlem  47101  hoiprodp1  47159  hoidmvlelem1  47166  hoidmvlelem2  47167  hoidmvlelem3  47168  hoidmvlelem4  47169  dfnbgrss2  48478  gsumsplit2f  48799  setrec1lem4  50308  elpglem2  50330