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

Syntax hints:   ∨ wo 847   ∈ wcel 2113   ∪ cun 3899   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  ssun2  4131  ssun3  4132  elun1  4134  difsssymdif  4215  inabs  4218  reuun1  4280  un00  4397  pwunss  4572  pwundif  4578  snsspr1  4770  snsstp1  4772  snsstp2  4773  uniintsn  4940  sofld  6145  sssucid  6399  fvrn0  6862  f1ounsn  7218  ovima0  7537  unexb  7692  unexbOLD  7693  dmexg  7843  resf1extb  7876  xpord2indlem  8089  xpord3inddlem  8096  suppun  8126  dftpos2  8185  tpostpos2  8189  frrlem12  8239  frrlem13  8240  tfrlem11  8319  oaabs2  8577  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  9587  cantnfp1lem3  9589  tc2  9649  unwf  9722  rankunb  9762  r0weon  9922  infxpenlem  9923  dfac2b  10041  djudoml  10095  cdainflem  10098  infunabs  10116  infdju  10117  infdif  10118  ackbij1lem15  10143  cfsmolem  10180  isfin4p1  10225  fin23lem11  10227  fin1a2lem10  10319  fin1a2lem13  10322  axdc3lem4  10363  axcclem  10367  zornn0g  10415  ttukeylem1  10419  ttukeylem5  10423  ttukeylem7  10425  fingch  10534  fpwwe2lem12  10553  gchac  10592  wunfi  10632  wundm  10639  wunex2  10649  inar1  10686  ressxr  11176  nnssnn0  12404  un0addcl  12434  un0mulcl  12435  nn0ssxnn0  12477  hashbclem  14375  hashf1lem1  14378  hashf1lem2  14379  ccatrn  14513  trclublem  14918  relexpdmg  14965  relexpaddg  14976  fsumsplit  15664  fsum2d  15694  fsumabs  15724  fsumrlim  15734  fsumo1  15735  incexclem  15759  fprodsplit  15889  fprod2d  15904  lcmfunsnlem1  16564  coprmprod  16588  vdwapid1  16903  vdwlem6  16914  ramcl2  16944  isstruct2  17076  srngbase  17230  srngplusg  17231  srngmulr  17232  lmodbase  17246  lmodplusg  17247  lmodsca  17248  ipsbase  17257  ipsaddg  17258  ipsmulr  17259  phlbase  17267  phlplusg  17268  phlsca  17269  odrngbas  17324  odrngplusg  17325  odrngmulr  17326  prdssca  17376  prdsbas  17377  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdsip  17381  prdsle  17382  prdsds  17384  prdstset  17386  imasbas  17433  imasplusg  17438  imasmulr  17439  imassca  17440  imasvsca  17441  imasip  17442  mreexexlem2d  17568  drsdirfi  18228  ipobas  18454  ipotset  18456  acsfiindd  18476  psdmrn  18496  dirdm  18523  grpinvfval  18908  mulgfval  18999  gsumzsplit  19856  gsumsplit2  19858  gsumzunsnd  19885  gsum2dlem2  19900  dprdfadd  19951  dmdprdsplit2lem  19976  dmdprdsplit2  19977  dmdprdsplit  19978  dprdsplit  19979  ablfac1eulem  20003  gsumle  20074  lspun  20938  lspsolv  21098  lsppratlem3  21104  islbs3  21110  lbsextlem2  21114  lbsextlem4  21116  cnfldbas  21313  mpocnfldadd  21314  mpocnfldmul  21316  cnfldcj  21318  cnfldtset  21319  cnfldle  21320  cnfldds  21321  cnfldbasOLD  21328  cnfldaddOLD  21329  cnfldmulOLD  21330  cnfldcjOLD  21331  cnfldtsetOLD  21332  cnfldleOLD  21333  cnflddsOLD  21334  psrbas  21889  psrplusg  21892  psrmulr  21898  mplsubglem  21954  mplcoe1  21992  mplcoe5  21995  mdetunilem9  22564  basdif0  22897  ordtbas2  23135  ordtbas  23136  ordtopn1  23138  leordtval2  23156  iocpnfordt  23159  icomnfordt  23160  uncmp  23347  fiuncmp  23348  bwth  23354  locfincmp  23470  comppfsc  23476  1stckgenlem  23497  1stckgen  23498  ptbasin  23521  ptbasfi  23525  dfac14lem  23561  dfac14  23562  ptuncnv  23751  ptunhmeo  23752  ptcmpfi  23757  fbun  23784  trfil2  23831  ufprim  23853  ufileu  23863  filufint  23864  ufildr  23875  fmfnfm  23902  hausflim  23925  fclsfnflim  23971  alexsubALTlem4  23994  tmdgsum  24039  tsmsgsum  24083  tsmsres  24088  tsmssplit  24096  tsmsxplem1  24097  ustssco  24159  ustuqtop1  24185  prdsxmetlem  24312  prdsbl  24435  icccmplem2  24768  fsumcn  24817  cnmpopc  24878  rrxmetlem  25363  rrxmet  25364  rrxdstprj1  25365  ovolctb2  25449  ovolunnul  25457  ovolfiniun  25458  nulmbl2  25493  finiunmbl  25501  volfiniun  25504  icombl  25521  ioombl  25522  uniiccdif  25535  mbfres2  25602  itg2splitlem  25705  itg2split  25706  itgfsum  25784  itgsplit  25793  itgsplitioo  25795  dvreslem  25866  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvmptfsum  25935  lhop  25977  dvcnvrelem2  25979  mdegcl  26030  elplyr  26162  plyrem  26269  xrlimcnp  26934  fsumharmonic  26978  chtdif  27124  lgsdir2lem3  27294  lgsquadlem2  27348  dchrisum0lem1b  27482  pntrlog2bndlem6  27550  pntlemf  27572  nosupinfsep  27700  noetalem1  27709  cutsun12  27786  cofcutrtime  27923  addsuniflem  27997  addbday  28014  negsval  28021  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  mulsuniflem  28145  mulsass  28162  precsexlem6  28208  precsexlem7  28209  precsexlem10  28212  precsexlem11  28213  ex-ss  30502  shsleji  31445  shsval2i  31462  ssjo  31522  sshhococi  31621  padct  32797  symgcom  33165  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  gsumvsca1  33308  gsumvsca2  33309  elrgspnsubrunlem1  33329  rlocbas  33349  rlocaddval  33350  rlocmulval  33351  elrspunsn  33510  mxidlprm  33551  idlsrgbas  33585  idlsrgplusg  33586  idlsrgmulr  33588  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  constrextdg2lem  33905  esumsplit  34210  esumpad2  34213  aean  34401  sxbrsigalem2  34443  bnj931  34926  tz9.1regs  35290  subfacp1lem2b  35375  subfacp1lem3  35376  subfacp1lem5  35378  kur14lem7  35406  kur14lem9  35408  cvmliftlem10  35488  satfsschain  35558  fmlasssuc  35583  refssfne  36552  filnetlem3  36574  bj-unrab  37127  bj-snglsstag  37182  bj-2upln0  37224  bj-ccssccbar  37422  rdgssun  37583  finixpnum  37806  matunitlindflem1  37817  mbfresfi  37867  prdsbnd  37994  heibor1lem  38010  rrnequiv  38036  paddunssN  40068  sspadd1  40075  sspadd2  40076  pclfinN  40160  dochdmj1  41650  dvhdimlem  41704  elrfi  42936  mzpcompact2lem  42993  eldioph2  43004  eldioph4b  43053  ttac  43278  pwssplit4  43331  pwslnmlem2  43335  isnumbasgrplem2  43346  algbase  43416  algaddg  43417  algmulr  43418  fiuneneq  43434  idomsubgmo  43435  onexlimgt  43485  omabs2  43574  tfsconcatrnss12  43591  rclexi  43856  rtrclex  43858  trclubgNEW  43859  trclexi  43861  rtrclexi  43862  cnvrcl0  43866  cnvtrcl0  43867  dfrtrcl5  43870  trrelsuperrel2dg  43912  dfrcl2  43915  relexp0a  43957  relexpaddss  43959  trclimalb2  43967  frege83d  43989  frege131d  44005  dssmapnvod  44261  clsk3nimkb  44281  isotone1  44289  grumnudlem  44526  dmwf  45206  infxrpnf  45690  mccllem  45843  cncfiooicclem1  46137  dvmptfprod  46189  dvnprodlem1  46190  iblsplit  46210  fourierdlem54  46404  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  sge0resplit  46650  sge0split  46653  sge0splitmpt  46655  sge0xaddlem1  46677  isomenndlem  46774  hoiprodp1  46832  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  dfnbgrss2  48105  gsumsplit2f  48426  setrec1lem4  49935  elpglem2  49957