Theorem ssun1 4125

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

Syntax hints:   ∨ wo 847   ∈ wcel 2111   ∪ cun 3895   ⊆ wss 3897

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914

This theorem is referenced by:  ssun2  4126  ssun3  4127  elun1  4129  difsssymdif  4210  inabs  4213  reuun1  4275  un00  4392  pwunss  4565  pwundif  4571  snsspr1  4763  snsstp1  4765  snsstp2  4766  uniintsn  4933  sofld  6134  sssucid  6388  fvrn0  6850  f1ounsn  7206  ovima0  7525  unexb  7680  unexbOLD  7681  dmexg  7831  resf1extb  7864  xpord2indlem  8077  xpord3inddlem  8084  suppun  8114  dftpos2  8173  tpostpos2  8177  frrlem12  8227  frrlem13  8228  tfrlem11  8307  oaabs2  8564  ralxpmap  8820  domss2  9049  mapunen  9059  ac6sfi  9168  frfi  9169  unfir  9192  domunfican  9206  iunfi  9227  elfiun  9314  dffi3  9315  unwdomg  9470  unxpwdom2  9474  unxpwdom  9475  cantnfp1lem1  9568  cantnfp1lem3  9570  tc2  9630  unwf  9703  rankunb  9743  r0weon  9903  infxpenlem  9904  dfac2b  10022  djudoml  10076  cdainflem  10079  infunabs  10097  infdju  10098  infdif  10099  ackbij1lem15  10124  cfsmolem  10161  isfin4p1  10206  fin23lem11  10208  fin1a2lem10  10300  fin1a2lem13  10303  axdc3lem4  10344  axcclem  10348  zornn0g  10396  ttukeylem1  10400  ttukeylem5  10404  ttukeylem7  10406  fingch  10514  fpwwe2lem12  10533  gchac  10572  wunfi  10612  wundm  10619  wunex2  10629  inar1  10666  ressxr  11156  nnssnn0  12384  un0addcl  12414  un0mulcl  12415  nn0ssxnn0  12457  hashbclem  14359  hashf1lem1  14362  hashf1lem2  14363  ccatrn  14497  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  18891  mulgfval  18982  gsumzsplit  19839  gsumsplit2  19841  gsumzunsnd  19868  gsum2dlem2  19883  dprdfadd  19934  dmdprdsplit2lem  19959  dmdprdsplit2  19960  dmdprdsplit  19961  dprdsplit  19962  ablfac1eulem  19986  gsumle  20057  lspun  20920  lspsolv  21080  lsppratlem3  21086  islbs3  21092  lbsextlem2  21096  lbsextlem4  21098  cnfldbas  21295  mpocnfldadd  21296  mpocnfldmul  21298  cnfldcj  21300  cnfldtset  21301  cnfldle  21302  cnfldds  21303  cnfldbasOLD  21310  cnfldaddOLD  21311  cnfldmulOLD  21312  cnfldcjOLD  21313  cnfldtsetOLD  21314  cnfldleOLD  21315  cnflddsOLD  21316  psrbas  21870  psrplusg  21873  psrmulr  21879  mplsubglem  21936  mplcoe1  21972  mplcoe5  21975  mdetunilem9  22535  basdif0  22868  ordtbas2  23106  ordtbas  23107  ordtopn1  23109  leordtval2  23127  iocpnfordt  23130  icomnfordt  23131  uncmp  23318  fiuncmp  23319  bwth  23325  locfincmp  23441  comppfsc  23447  1stckgenlem  23468  1stckgen  23469  ptbasin  23492  ptbasfi  23496  dfac14lem  23532  dfac14  23533  ptuncnv  23722  ptunhmeo  23723  ptcmpfi  23728  fbun  23755  trfil2  23802  ufprim  23824  ufileu  23834  filufint  23835  ufildr  23846  fmfnfm  23873  hausflim  23896  fclsfnflim  23942  alexsubALTlem4  23965  tmdgsum  24010  tsmsgsum  24054  tsmsres  24059  tsmssplit  24067  tsmsxplem1  24068  ustssco  24130  ustuqtop1  24156  prdsxmetlem  24283  prdsbl  24406  icccmplem2  24739  fsumcn  24788  cnmpopc  24849  rrxmetlem  25334  rrxmet  25335  rrxdstprj1  25336  ovolctb2  25420  ovolunnul  25428  ovolfiniun  25429  nulmbl2  25464  finiunmbl  25472  volfiniun  25475  icombl  25492  ioombl  25493  uniiccdif  25506  mbfres2  25573  itg2splitlem  25676  itg2split  25677  itgfsum  25755  itgsplit  25764  itgsplitioo  25766  dvreslem  25837  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvmptfsum  25906  lhop  25948  dvcnvrelem2  25950  mdegcl  26001  elplyr  26133  plyrem  26240  xrlimcnp  26905  fsumharmonic  26949  chtdif  27095  lgsdir2lem3  27265  lgsquadlem2  27319  dchrisum0lem1b  27453  pntrlog2bndlem6  27521  pntlemf  27543  nosupinfsep  27671  noetalem1  27680  scutun12  27751  cofcutrtime  27871  addsuniflem  27944  addsbday  27960  negsval  27967  mulsproplem12  28066  mulsproplem13  28067  mulsproplem14  28068  mulsuniflem  28088  mulsass  28105  precsexlem6  28150  precsexlem7  28151  precsexlem10  28154  precsexlem11  28155  ex-ss  30407  shsleji  31350  shsval2i  31367  ssjo  31427  sshhococi  31526  padct  32701  symgcom  33052  cycpmco2lem5  33099  cycpmco2lem6  33100  cycpmco2lem7  33101  cycpmco2  33102  gsumvsca1  33195  gsumvsca2  33196  elrgspnsubrunlem1  33214  rlocbas  33234  rlocaddval  33235  rlocmulval  33236  elrspunsn  33394  mxidlprm  33435  idlsrgbas  33469  idlsrgplusg  33470  idlsrgmulr  33472  fldextrspundgdvdslem  33693  fldextrspundgdvds  33694  constrextdg2lem  33761  esumsplit  34066  esumpad2  34069  aean  34257  sxbrsigalem2  34299  bnj931  34782  tz9.1regs  35130  subfacp1lem2b  35225  subfacp1lem3  35226  subfacp1lem5  35228  kur14lem7  35256  kur14lem9  35258  cvmliftlem10  35338  satfsschain  35408  fmlasssuc  35433  refssfne  36400  filnetlem3  36422  bj-unrab  36968  bj-snglsstag  37023  bj-2upln0  37065  bj-ccssccbar  37259  rdgssun  37420  finixpnum  37653  matunitlindflem1  37664  mbfresfi  37714  prdsbnd  37841  heibor1lem  37857  rrnequiv  37883  paddunssN  39855  sspadd1  39862  sspadd2  39863  pclfinN  39947  dochdmj1  41437  dvhdimlem  41491  elrfi  42735  mzpcompact2lem  42792  eldioph2  42803  eldioph4b  42852  ttac  43077  pwssplit4  43130  pwslnmlem2  43134  isnumbasgrplem2  43145  algbase  43215  algaddg  43216  algmulr  43217  fiuneneq  43233  idomsubgmo  43234  onexlimgt  43284  omabs2  43373  tfsconcatrnss12  43390  rclexi  43656  rtrclex  43658  trclubgNEW  43659  trclexi  43661  rtrclexi  43662  cnvrcl0  43666  cnvtrcl0  43667  dfrtrcl5  43670  trrelsuperrel2dg  43712  dfrcl2  43715  relexp0a  43757  relexpaddss  43759  trclimalb2  43767  frege83d  43789  frege131d  43805  dssmapnvod  44061  clsk3nimkb  44081  isotone1  44089  grumnudlem  44326  dmwf  45006  infxrpnf  45492  mccllem  45645  cncfiooicclem1  45939  dvmptfprod  45991  dvnprodlem1  45992  iblsplit  46012  fourierdlem54  46206  fourierdlem102  46254  fourierdlem103  46255  fourierdlem104  46256  fourierdlem114  46266  sge0resplit  46452  sge0split  46455  sge0splitmpt  46457  sge0xaddlem1  46479  isomenndlem  46576  hoiprodp1  46634  hoidmvlelem1  46641  hoidmvlelem2  46642  hoidmvlelem3  46643  hoidmvlelem4  46644  dfnbgrss2  47898  gsumsplit2f  48219  setrec1lem4  49730  elpglem2  49752