Theorem ssun1 4129

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

Syntax hints:   ∨ wo 847   ∈ wcel 2109   ∪ cun 3901   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920

This theorem is referenced by:  ssun2  4130  ssun3  4131  elun1  4133  difsssymdif  4214  inabs  4217  reuun1  4279  un00  4396  pwunss  4569  pwundif  4575  snsspr1  4765  snsstp1  4767  snsstp2  4768  uniintsn  4935  sofld  6136  sssucid  6389  fvrn0  6850  f1ounsn  7209  ovima0  7528  unexb  7683  unexbOLD  7684  dmexg  7834  resf1extb  7867  xpord2indlem  8080  xpord3inddlem  8087  suppun  8117  dftpos2  8176  tpostpos2  8180  frrlem12  8230  frrlem13  8231  tfrlem11  8310  oaabs2  8567  ralxpmap  8823  domss2  9053  mapunen  9063  ac6sfi  9173  frfi  9174  unfir  9197  domunfican  9211  iunfi  9233  elfiun  9320  dffi3  9321  unwdomg  9476  unxpwdom2  9480  unxpwdom  9481  cantnfp1lem1  9574  cantnfp1lem3  9576  tc2  9638  unwf  9706  rankunb  9746  r0weon  9906  infxpenlem  9907  dfac2b  10025  djudoml  10079  cdainflem  10082  infunabs  10100  infdju  10101  infdif  10102  ackbij1lem15  10127  cfsmolem  10164  isfin4p1  10209  fin23lem11  10211  fin1a2lem10  10303  fin1a2lem13  10306  axdc3lem4  10347  axcclem  10351  zornn0g  10399  ttukeylem1  10403  ttukeylem5  10407  ttukeylem7  10409  fingch  10517  fpwwe2lem12  10536  gchac  10575  wunfi  10615  wundm  10622  wunex2  10632  inar1  10669  ressxr  11159  nnssnn0  12387  un0addcl  12417  un0mulcl  12418  nn0ssxnn0  12460  hashbclem  14359  hashf1lem1  14362  hashf1lem2  14363  ccatrn  14496  trclublem  14902  relexpdmg  14949  relexpaddg  14960  fsumsplit  15648  fsum2d  15678  fsumabs  15708  fsumrlim  15718  fsumo1  15719  incexclem  15743  fprodsplit  15873  fprod2d  15888  lcmfunsnlem1  16548  coprmprod  16572  vdwapid1  16887  vdwlem6  16898  ramcl2  16928  isstruct2  17060  srngbase  17214  srngplusg  17215  srngmulr  17216  lmodbase  17230  lmodplusg  17231  lmodsca  17232  ipsbase  17241  ipsaddg  17242  ipsmulr  17243  phlbase  17251  phlplusg  17252  phlsca  17253  odrngbas  17308  odrngplusg  17309  odrngmulr  17310  prdssca  17360  prdsbas  17361  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdsip  17365  prdsle  17366  prdsds  17368  prdstset  17370  imasbas  17416  imasplusg  17421  imasmulr  17422  imassca  17423  imasvsca  17424  imasip  17425  mreexexlem2d  17551  drsdirfi  18211  ipobas  18437  ipotset  18439  acsfiindd  18459  psdmrn  18479  dirdm  18506  grpinvfval  18857  mulgfval  18948  gsumzsplit  19806  gsumsplit2  19808  gsumzunsnd  19835  gsum2dlem2  19850  dprdfadd  19901  dmdprdsplit2lem  19926  dmdprdsplit2  19927  dmdprdsplit  19928  dprdsplit  19929  ablfac1eulem  19953  gsumle  20024  lspun  20890  lspsolv  21050  lsppratlem3  21056  islbs3  21062  lbsextlem2  21066  lbsextlem4  21068  cnfldbas  21265  mpocnfldadd  21266  mpocnfldmul  21268  cnfldcj  21270  cnfldtset  21271  cnfldle  21272  cnfldds  21273  cnfldbasOLD  21280  cnfldaddOLD  21281  cnfldmulOLD  21282  cnfldcjOLD  21283  cnfldtsetOLD  21284  cnfldleOLD  21285  cnflddsOLD  21286  psrbas  21840  psrplusg  21843  psrmulr  21849  mplsubglem  21906  mplcoe1  21942  mplcoe5  21945  mdetunilem9  22505  basdif0  22838  ordtbas2  23076  ordtbas  23077  ordtopn1  23079  leordtval2  23097  iocpnfordt  23100  icomnfordt  23101  uncmp  23288  fiuncmp  23289  bwth  23295  locfincmp  23411  comppfsc  23417  1stckgenlem  23438  1stckgen  23439  ptbasin  23462  ptbasfi  23466  dfac14lem  23502  dfac14  23503  ptuncnv  23692  ptunhmeo  23693  ptcmpfi  23698  fbun  23725  trfil2  23772  ufprim  23794  ufileu  23804  filufint  23805  ufildr  23816  fmfnfm  23843  hausflim  23866  fclsfnflim  23912  alexsubALTlem4  23935  tmdgsum  23980  tsmsgsum  24024  tsmsres  24029  tsmssplit  24037  tsmsxplem1  24038  ustssco  24100  ustuqtop1  24127  prdsxmetlem  24254  prdsbl  24377  icccmplem2  24710  fsumcn  24759  cnmpopc  24820  rrxmetlem  25305  rrxmet  25306  rrxdstprj1  25307  ovolctb2  25391  ovolunnul  25399  ovolfiniun  25400  nulmbl2  25435  finiunmbl  25443  volfiniun  25446  icombl  25463  ioombl  25464  uniiccdif  25477  mbfres2  25544  itg2splitlem  25647  itg2split  25648  itgfsum  25726  itgsplit  25735  itgsplitioo  25737  dvreslem  25808  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvmptfsum  25877  lhop  25919  dvcnvrelem2  25921  mdegcl  25972  elplyr  26104  plyrem  26211  xrlimcnp  26876  fsumharmonic  26920  chtdif  27066  lgsdir2lem3  27236  lgsquadlem2  27290  dchrisum0lem1b  27424  pntrlog2bndlem6  27492  pntlemf  27514  nosupinfsep  27642  noetalem1  27651  scutun12  27721  cofcutrtime  27840  addsuniflem  27913  addsbday  27929  negsval  27936  mulsproplem12  28035  mulsproplem13  28036  mulsproplem14  28037  mulsuniflem  28057  mulsass  28074  precsexlem6  28119  precsexlem7  28120  precsexlem10  28123  precsexlem11  28124  ex-ss  30371  shsleji  31314  shsval2i  31331  ssjo  31391  sshhococi  31490  padct  32662  symgcom  33025  cycpmco2lem5  33072  cycpmco2lem6  33073  cycpmco2lem7  33074  cycpmco2  33075  gsumvsca1  33168  gsumvsca2  33169  elrgspnsubrunlem1  33187  rlocbas  33207  rlocaddval  33208  rlocmulval  33209  elrspunsn  33366  mxidlprm  33407  idlsrgbas  33441  idlsrgplusg  33442  idlsrgmulr  33444  fldextrspundgdvdslem  33647  fldextrspundgdvds  33648  constrextdg2lem  33715  esumsplit  34020  esumpad2  34023  aean  34211  sxbrsigalem2  34254  bnj931  34737  tz9.1regs  35067  subfacp1lem2b  35154  subfacp1lem3  35155  subfacp1lem5  35157  kur14lem7  35185  kur14lem9  35187  cvmliftlem10  35267  satfsschain  35337  fmlasssuc  35362  refssfne  36332  filnetlem3  36354  bj-unrab  36900  bj-snglsstag  36955  bj-2upln0  36997  bj-ccssccbar  37191  rdgssun  37352  finixpnum  37585  matunitlindflem1  37596  mbfresfi  37646  prdsbnd  37773  heibor1lem  37789  rrnequiv  37815  paddunssN  39787  sspadd1  39794  sspadd2  39795  pclfinN  39879  dochdmj1  41369  dvhdimlem  41423  elrfi  42667  mzpcompact2lem  42724  eldioph2  42735  eldioph4b  42784  ttac  43009  pwssplit4  43062  pwslnmlem2  43066  isnumbasgrplem2  43077  algbase  43147  algaddg  43148  algmulr  43149  fiuneneq  43165  idomsubgmo  43166  onexlimgt  43216  omabs2  43305  tfsconcatrnss12  43322  rclexi  43588  rtrclex  43590  trclubgNEW  43591  trclexi  43593  rtrclexi  43594  cnvrcl0  43598  cnvtrcl0  43599  dfrtrcl5  43602  trrelsuperrel2dg  43644  dfrcl2  43647  relexp0a  43689  relexpaddss  43691  trclimalb2  43699  frege83d  43721  frege131d  43737  dssmapnvod  43993  clsk3nimkb  44013  isotone1  44021  grumnudlem  44258  dmwf  44939  infxrpnf  45425  mccllem  45578  cncfiooicclem1  45874  dvmptfprod  45926  dvnprodlem1  45927  iblsplit  45947  fourierdlem54  46141  fourierdlem102  46189  fourierdlem103  46190  fourierdlem104  46191  fourierdlem114  46201  sge0resplit  46387  sge0split  46390  sge0splitmpt  46392  sge0xaddlem1  46414  isomenndlem  46511  hoiprodp1  46569  hoidmvlelem1  46576  hoidmvlelem2  46577  hoidmvlelem3  46578  hoidmvlelem4  46579  dfnbgrss2  47843  gsumsplit2f  48164  setrec1lem4  49675  elpglem2  49697