Theorem ssun1 4128

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

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

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916

This theorem is referenced by:  ssun2  4129  ssun3  4130  elun1  4132  difsssymdif  4213  inabs  4216  reuun1  4278  un00  4395  pwunss  4570  pwundif  4576  snsspr1  4768  snsstp1  4770  snsstp2  4771  uniintsn  4938  sofld  6143  sssucid  6397  fvrn0  6860  f1ounsn  7216  ovima0  7535  unexb  7690  unexbOLD  7691  dmexg  7841  resf1extb  7874  xpord2indlem  8087  xpord3inddlem  8094  suppun  8124  dftpos2  8183  tpostpos2  8187  frrlem12  8237  frrlem13  8238  tfrlem11  8317  oaabs2  8575  ralxpmap  8832  domss2  9062  mapunen  9072  ac6sfi  9182  frfi  9183  unfir  9206  domunfican  9220  iunfi  9241  elfiun  9331  dffi3  9332  unwdomg  9487  unxpwdom2  9491  unxpwdom  9492  cantnfp1lem1  9585  cantnfp1lem3  9587  tc2  9647  unwf  9720  rankunb  9760  r0weon  9920  infxpenlem  9921  dfac2b  10039  djudoml  10093  cdainflem  10096  infunabs  10114  infdju  10115  infdif  10116  ackbij1lem15  10141  cfsmolem  10178  isfin4p1  10223  fin23lem11  10225  fin1a2lem10  10317  fin1a2lem13  10320  axdc3lem4  10361  axcclem  10365  zornn0g  10413  ttukeylem1  10417  ttukeylem5  10421  ttukeylem7  10423  fingch  10532  fpwwe2lem12  10551  gchac  10590  wunfi  10630  wundm  10637  wunex2  10647  inar1  10684  ressxr  11174  nnssnn0  12402  un0addcl  12432  un0mulcl  12433  nn0ssxnn0  12475  hashbclem  14373  hashf1lem1  14376  hashf1lem2  14377  ccatrn  14511  trclublem  14916  relexpdmg  14963  relexpaddg  14974  fsumsplit  15662  fsum2d  15692  fsumabs  15722  fsumrlim  15732  fsumo1  15733  incexclem  15757  fprodsplit  15887  fprod2d  15902  lcmfunsnlem1  16562  coprmprod  16586  vdwapid1  16901  vdwlem6  16912  ramcl2  16942  isstruct2  17074  srngbase  17228  srngplusg  17229  srngmulr  17230  lmodbase  17244  lmodplusg  17245  lmodsca  17246  ipsbase  17255  ipsaddg  17256  ipsmulr  17257  phlbase  17265  phlplusg  17266  phlsca  17267  odrngbas  17322  odrngplusg  17323  odrngmulr  17324  prdssca  17374  prdsbas  17375  prdsplusg  17376  prdsmulr  17377  prdsvsca  17378  prdsip  17379  prdsle  17380  prdsds  17382  prdstset  17384  imasbas  17431  imasplusg  17436  imasmulr  17437  imassca  17438  imasvsca  17439  imasip  17440  mreexexlem2d  17566  drsdirfi  18226  ipobas  18452  ipotset  18454  acsfiindd  18474  psdmrn  18494  dirdm  18521  grpinvfval  18906  mulgfval  18997  gsumzsplit  19854  gsumsplit2  19856  gsumzunsnd  19883  gsum2dlem2  19898  dprdfadd  19949  dmdprdsplit2lem  19974  dmdprdsplit2  19975  dmdprdsplit  19976  dprdsplit  19977  ablfac1eulem  20001  gsumle  20072  lspun  20936  lspsolv  21096  lsppratlem3  21102  islbs3  21108  lbsextlem2  21112  lbsextlem4  21114  cnfldbas  21311  mpocnfldadd  21312  mpocnfldmul  21314  cnfldcj  21316  cnfldtset  21317  cnfldle  21318  cnfldds  21319  cnfldbasOLD  21326  cnfldaddOLD  21327  cnfldmulOLD  21328  cnfldcjOLD  21329  cnfldtsetOLD  21330  cnfldleOLD  21331  cnflddsOLD  21332  psrbas  21887  psrplusg  21890  psrmulr  21896  mplsubglem  21952  mplcoe1  21990  mplcoe5  21993  mdetunilem9  22562  basdif0  22895  ordtbas2  23133  ordtbas  23134  ordtopn1  23136  leordtval2  23154  iocpnfordt  23157  icomnfordt  23158  uncmp  23345  fiuncmp  23346  bwth  23352  locfincmp  23468  comppfsc  23474  1stckgenlem  23495  1stckgen  23496  ptbasin  23519  ptbasfi  23523  dfac14lem  23559  dfac14  23560  ptuncnv  23749  ptunhmeo  23750  ptcmpfi  23755  fbun  23782  trfil2  23829  ufprim  23851  ufileu  23861  filufint  23862  ufildr  23873  fmfnfm  23900  hausflim  23923  fclsfnflim  23969  alexsubALTlem4  23992  tmdgsum  24037  tsmsgsum  24081  tsmsres  24086  tsmssplit  24094  tsmsxplem1  24095  ustssco  24157  ustuqtop1  24183  prdsxmetlem  24310  prdsbl  24433  icccmplem2  24766  fsumcn  24815  cnmpopc  24876  rrxmetlem  25361  rrxmet  25362  rrxdstprj1  25363  ovolctb2  25447  ovolunnul  25455  ovolfiniun  25456  nulmbl2  25491  finiunmbl  25499  volfiniun  25502  icombl  25519  ioombl  25520  uniiccdif  25533  mbfres2  25600  itg2splitlem  25703  itg2split  25704  itgfsum  25782  itgsplit  25791  itgsplitioo  25793  dvreslem  25864  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  dvmptfsum  25933  lhop  25975  dvcnvrelem2  25977  mdegcl  26028  elplyr  26160  plyrem  26267  xrlimcnp  26932  fsumharmonic  26976  chtdif  27122  lgsdir2lem3  27292  lgsquadlem2  27346  dchrisum0lem1b  27480  pntrlog2bndlem6  27548  pntlemf  27570  nosupinfsep  27698  noetalem1  27707  scutun12  27778  cofcutrtime  27898  addsuniflem  27971  addsbday  27987  negsval  27994  mulsproplem12  28096  mulsproplem13  28097  mulsproplem14  28098  mulsuniflem  28118  mulsass  28135  precsexlem6  28180  precsexlem7  28181  precsexlem10  28184  precsexlem11  28185  ex-ss  30451  shsleji  31394  shsval2i  31411  ssjo  31471  sshhococi  31570  padct  32746  symgcom  33114  cycpmco2lem5  33161  cycpmco2lem6  33162  cycpmco2lem7  33163  cycpmco2  33164  gsumvsca1  33257  gsumvsca2  33258  elrgspnsubrunlem1  33278  rlocbas  33298  rlocaddval  33299  rlocmulval  33300  elrspunsn  33459  mxidlprm  33500  idlsrgbas  33534  idlsrgplusg  33535  idlsrgmulr  33537  fldextrspundgdvdslem  33786  fldextrspundgdvds  33787  constrextdg2lem  33854  esumsplit  34159  esumpad2  34162  aean  34350  sxbrsigalem2  34392  bnj931  34875  tz9.1regs  35239  subfacp1lem2b  35324  subfacp1lem3  35325  subfacp1lem5  35327  kur14lem7  35355  kur14lem9  35357  cvmliftlem10  35437  satfsschain  35507  fmlasssuc  35532  refssfne  36501  filnetlem3  36523  bj-unrab  37070  bj-snglsstag  37125  bj-2upln0  37167  bj-ccssccbar  37361  rdgssun  37522  finixpnum  37745  matunitlindflem1  37756  mbfresfi  37806  prdsbnd  37933  heibor1lem  37949  rrnequiv  37975  paddunssN  40007  sspadd1  40014  sspadd2  40015  pclfinN  40099  dochdmj1  41589  dvhdimlem  41643  elrfi  42878  mzpcompact2lem  42935  eldioph2  42946  eldioph4b  42995  ttac  43220  pwssplit4  43273  pwslnmlem2  43277  isnumbasgrplem2  43288  algbase  43358  algaddg  43359  algmulr  43360  fiuneneq  43376  idomsubgmo  43377  onexlimgt  43427  omabs2  43516  tfsconcatrnss12  43533  rclexi  43798  rtrclex  43800  trclubgNEW  43801  trclexi  43803  rtrclexi  43804  cnvrcl0  43808  cnvtrcl0  43809  dfrtrcl5  43812  trrelsuperrel2dg  43854  dfrcl2  43857  relexp0a  43899  relexpaddss  43901  trclimalb2  43909  frege83d  43931  frege131d  43947  dssmapnvod  44203  clsk3nimkb  44223  isotone1  44231  grumnudlem  44468  dmwf  45148  infxrpnf  45632  mccllem  45785  cncfiooicclem1  46079  dvmptfprod  46131  dvnprodlem1  46132  iblsplit  46152  fourierdlem54  46346  fourierdlem102  46394  fourierdlem103  46395  fourierdlem104  46396  fourierdlem114  46406  sge0resplit  46592  sge0split  46595  sge0splitmpt  46597  sge0xaddlem1  46619  isomenndlem  46716  hoiprodp1  46774  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem3  46783  hoidmvlelem4  46784  dfnbgrss2  48047  gsumsplit2f  48368  setrec1lem4  49877  elpglem2  49899