Theorem ssun1 4124

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

This proof depends on syntax axioms:   ∨ wo 861   ∈ wcel 2145   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  ssun2  4125  ssun3  4126  elun1  4128  difsssymdif  4209  inabs  4212  reuun1  4274  un00  4357  pwunss  4575  pwundif  4582  snsspr1  4775  snsstp1  4777  snsstp2  4778  uniintsn  4945  sofld  6179  relresfld  6278  sssucid  6445  fvrn0  6913  f1ounsn  7280  ovima0  7600  unexb  7763  dmexg  7913  resf1extb  7946  xpord2indlem  8164  xpord3inddlem  8171  suppun  8201  dftpos2  8260  tpostpos2  8264  frrlem12  8315  frrlem13  8316  tfrlem11  8396  oaabs2  8658  ralxpmap  8924  domss2  9155  mapunen  9165  ac6sfi  9275  frfi  9276  unfir  9300  domunfican  9313  iunfi  9332  elfiun  9422  dffi3  9423  unwdomg  9578  unxpwdom2  9582  unxpwdom  9583  cantnfp1lem1  9679  cantnfp1lem3  9681  tc2  9741  unwf  9818  rankunb  9864  setrec1lem4  9971  r0weon  10091  infxpenlem  10092  dfac2b  10209  djudoml  10263  cdainflem  10266  infunabs  10284  infdju  10285  infdif  10286  ackbij1lem15  10311  cfsmolem  10348  isfin4p1  10393  fin23lem11  10395  fin1a2lem10  10487  fin1a2lem13  10490  axdc3lem4  10531  axcclem  10535  zornn0g  10583  ttukeylem1  10587  ttukeylem5  10591  ttukeylem7  10593  fingch  10708  fpwwe2lem12  10727  gchac  10766  wunfi  10806  wundm  10813  wunex2  10823  inar1  10860  ressxr  11353  nnssnn0  12609  un0addcl  12639  un0mulcl  12640  nn0ssxnn0  12682  hashbclem  14597  hashf1lem1  14600  hashf1lem2  14601  ccatrn  14735  trclublem  15148  relexpdmg  15195  relexpaddg  15206  fsumsplit  15907  fsum2d  15937  fsumabs  15968  fsumrlim  15978  fsumo1  15979  incexclem  16005  fprodsplit  16133  fprod2d  16148  lcmfunsnlem1  16812  coprmprod  16836  vdwapid1  17153  vdwlem6  17164  ramcl2  17194  isstruct2  17327  srngbase  17481  srngplusg  17482  srngmulr  17483  lmodbase  17497  lmodplusg  17498  lmodsca  17499  ipsbase  17508  ipsaddg  17509  ipsmulr  17510  phlbase  17518  phlplusg  17519  phlsca  17520  odrngbas  17575  odrngplusg  17576  odrngmulr  17577  prdssca  17627  prdsbas  17628  prdsplusg  17629  prdsmulr  17630  prdsvsca  17631  prdsip  17632  prdsle  17633  prdsds  17635  prdstset  17637  imasbas  17684  imasplusg  17689  imasmulr  17690  imassca  17691  imasvsca  17692  imasip  17693  mreexexlem2d  17819  drsdirfi  18479  ipobas  18705  ipotset  18707  acsfiindd  18727  psdmrn  18747  dirdm  18774  grpinvfval  19189  mulgfval  19279  gsumzsplit  20141  gsumsplit2  20143  gsumzunsnd  20170  gsum2dlem2  20185  dprdfadd  20236  dmdprdsplit2lem  20261  dmdprdsplit2  20262  dmdprdsplit  20263  dprdsplit  20264  ablfac1eulem  20288  gsumle  20359  lspun  21262  lspsolv  21421  lsppratlem3  21427  islbs3  21433  lbsextlem2  21437  lbsextlem4  21439  cnfldbas  21682  mpocnfldadd  21683  mpocnfldmul  21685  cnfldcj  21687  cnfldtset  21688  cnfldle  21689  cnfldds  21690  psrbas  22242  psrplusg  22245  psrmulr  22250  mplsubglem  22306  mplcoe1  22346  mplcoe5  22349  mdetunilem9  22935  matunitlindflem1  22994  basdif0  23271  ordtbas2  23509  ordtbas  23510  ordtopn1  23512  leordtval2  23530  iocpnfordt  23533  icomnfordt  23534  uncmp  23721  fiuncmp  23722  bwth  23728  locfincmp  23845  comppfsc  23851  1stckgenlem  23872  1stckgen  23873  ptbasin  23896  ptbasfi  23900  dfac14lem  23936  dfac14  23937  ptuncnv  24126  ptunhmeo  24127  ptcmpfi  24132  fbun  24159  trfil2  24206  ufprim  24228  ufileu  24238  filufint  24239  ufildr  24250  fmfnfm  24277  hausflim  24300  fclsfnflim  24346  alexsubALTlem4  24369  tmdgsum  24414  tsmsgsum  24458  tsmsres  24463  tsmssplit  24471  tsmsxplem1  24472  ustssco  24534  ustuqtop1  24560  prdsxmetlem  24687  prdsbl  24810  icccmplem2  25143  fsumcn  25191  cnmpopc  25249  rrxmetlem  25728  rrxmet  25729  rrxdstprj1  25730  ovolctb2  25813  ovolunnul  25821  ovolfiniun  25822  nulmbl2  25857  finiunmbl  25865  volfiniun  25868  icombl  25885  ioombl  25886  uniiccdif  25899  mbfres2  25966  itg2splitlem  26069  itg2split  26070  itgfsum  26147  itgsplit  26156  itgsplitioo  26158  dvreslem  26229  dvaddbr  26258  dvmulbr  26259  dvmptfsum  26295  lhop  26336  dvcnvrelem2  26338  mdegcl  26387  elplyr  26519  plyrem  26626  xrlimcnp  27296  fsumharmonic  27339  chtdif  27485  lgsdir2lem3  27654  lgsquadlem2  27708  dchrisum0lem1b  27842  pntrlog2bndlem6  27910  pntlemf  27932  nosupinfsep  28089  noetalem1  28098  cutsun12  28176  cofcutrtime  28313  addsuniflem  28387  addbday  28404  negsval  28411  mulsproplem12  28513  mulsproplem13  28514  mulsproplem14  28515  mulsuniflem  28535  mulsass  28552  precsexlem6  28598  precsexlem7  28599  precsexlem10  28602  precsexlem11  28603  ex-ss  31028  shsleji  31972  shsval2i  31989  ssjo  32049  sshhococi  32148  padct  33310  symgcom  33644  cycpmco2lem5  33691  cycpmco2lem6  33692  cycpmco2lem7  33693  cycpmco2  33694  gsumvsca1  33787  gsumvsca2  33788  elrgspnsubrunlem1  33808  rlocbas  33829  rlocaddval  33830  rlocmulval  33831  elrspunsn  33979  mxidlprm  33995  idlsrgbas  34036  idlsrgplusg  34037  idlsrgmulr  34039  fldextrspundgdvdslem  34312  fldextrspundgdvds  34313  constrextdg2lem  34380  esumsplit  34685  esumpad2  34688  aean  34877  sxbrsigalem2  34918  bnj931  35401  tz9.1regs  35802  subfacp1lem2b  35946  subfacp1lem3  35947  subfacp1lem5  35949  kur14lem7  35977  kur14lem9  35979  cvmliftlem10  36059  satfsschain  36129  fmlasssuc  36154  refssfne  37146  filnetlem3  37168  bj-unrab  37839  bj-snglsstag  37894  bj-2upln0  37936  bj-ccssccbar  38138  rdgssun  38301  finixpnum  38528  mbfresfi  38584  prdsbnd  38727  heibor1lem  38743  rrnequiv  38769  paddunssN  40865  sspadd1  40872  sspadd2  40873  pclfinN  40957  dochdmj1  42447  dvhdimlem  42501  elrfi  43704  mzpcompact2lem  43761  eldioph2  43772  eldioph4b  43817  ttac  44042  pwssplit4  44090  pwslnmlem2  44094  isnumbasgrplem2  44105  algbase  44175  algaddg  44176  algmulr  44177  fiuneneq  44193  idomsubgmo  44194  onexlimgt  44244  omabs2  44333  tfsconcatrnss12  44350  rclexi  44614  rtrclex  44616  trclubgNEW  44617  trclexi  44619  rtrclexi  44620  cnvrcl0  44624  cnvtrcl0  44625  dfrtrcl5  44628  trrelsuperrel2dg  44670  dfrcl2  44673  relexp0a  44715  relexpaddss  44717  trclimalb2  44725  frege83d  44747  frege131d  44763  dssmapnvod  45019  clsk3nimkb  45039  isotone1  45047  grumnudlem  45268  dmwf  45954  hfdm  46017  infxrpnf  46455  mccllem  46608  cncfiooicclem1  46902  dvmptfprod  46954  dvnprodlem1  46955  iblsplit  46975  fourierdlem54  47169  fourierdlem102  47217  fourierdlem103  47218  fourierdlem104  47219  fourierdlem114  47229  sge0resplit  47415  sge0split  47418  sge0splitmpt  47420  sge0xaddlem1  47442  isomenndlem  47539  hoiprodp1  47597  hoidmvlelem1  47604  hoidmvlelem2  47605  hoidmvlelem3  47606  hoidmvlelem4  47607  wrddun  47898  chndun  47903  chnrun  47908  dfnbgrss2  48956  gsumsplit2f  49276  elpglem2  50804