Theorem ssun1 4179

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

This proof depends on syntax axioms:   ∨ wo 861   ∈ wcel 2147   ⊆ wss 3900   ∪ cun 4152

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154

This theorem is used by:  ssun2  4180  ssun3  4181  elun1  4183  difsssymdif  4211  inabs  4214  reuun1  4276  un00  4360  pwunss  4579  pwundif  4586  snsspr1  4775  snsstp1  4777  snsstp2  4778  uniintsn  4950  sofld  6197  relresfld  6302  sssucid  6471  fununfun  6616  fvrn0  6944  f1ounsn  7311  ovima0  7632  unexb  7795  dmexg  7947  resf1extb  7980  xpord2indlem  8201  xpord3inddlem  8208  suppun  8239  dftpos2  8298  tpostpos2  8302  frrlem12  8353  frrlem13  8354  tfrlem11  8434  oaabs2  8696  ralxpmap  8962  domss2  9193  mapunen  9203  ac6sfi  9313  frfi  9314  unfir  9338  domunfican  9351  iunfi  9370  elfiun  9459  dffi3  9460  unwdomg  9615  unxpwdom2  9619  unxpwdom  9620  cantnfp1lem1  9716  cantnfp1lem3  9718  tc2  9778  unwf  9855  rankunb  9901  setrec1lem4  10008  r0weon  10130  infxpenlem  10131  dfac2b  10248  djudoml  10302  cdainflem  10305  infunabs  10323  infdju  10324  infdif  10325  ackbij1lem15  10350  cfsmolem  10387  isfin4p1  10432  fin23lem11  10434  fin1a2lem10  10526  fin1a2lem13  10529  axdc3lem4  10570  axcclem  10574  zornn0g  10622  ttukeylem1  10626  ttukeylem5  10630  ttukeylem7  10632  fingch  10747  fpwwe2lem12  10766  gchac  10805  wunfi  10845  wundm  10852  wunex2  10862  inar1  10899  ressxr  11392  nnssnn0  12649  un0addcl  12679  un0mulcl  12680  nn0ssxnn0  12722  hashbclem  14638  hashf1lem1  14641  hashf1lem2  14642  ccatrn  14776  trclublem  15191  relexpdmg  15238  relexpaddg  15249  fsumsplit  15951  fsum2d  15981  fsumabs  16012  fsumrlim  16022  fsumo1  16023  incexclem  16049  fprodsplit  16177  fprod2d  16192  lcmfunsnlem1  16856  coprmprod  16880  vdwapid1  17197  vdwlem6  17208  ramcl2  17238  isstruct2  17371  srngbase  17527  srngplusg  17528  srngmulr  17529  lmodbase  17543  lmodplusg  17544  lmodsca  17545  ipsbase  17554  ipsaddg  17555  ipsmulr  17556  phlbase  17564  phlplusg  17565  phlsca  17566  odrngbas  17621  odrngplusg  17622  odrngmulr  17623  prdssca  17677  prdsbas  17678  prdsplusg  17679  prdsmulr  17680  prdsvsca  17681  prdsip  17682  prdsle  17683  prdsds  17685  prdstset  17687  imasbas  17734  imasplusg  17739  imasmulr  17740  imassca  17741  imasvsca  17742  imasip  17743  mreexexlem2d  17869  drsdirfi  18529  ipobas  18755  ipotset  18757  acsfiindd  18777  psdmrn  18797  dirdm  18824  grpinvfval  19239  mulgfval  19329  gsumzsplit  20192  gsumsplit2  20194  gsumzunsnd  20221  gsum2dlem2  20236  dprdfadd  20287  dmdprdsplit2lem  20312  dmdprdsplit2  20313  dmdprdsplit  20314  dprdsplit  20315  ablfac1eulem  20339  gsumle  20410  lspun  21313  lspsolv  21472  lsppratlem3  21478  islbs3  21484  lbsextlem2  21488  lbsextlem4  21490  cnfldbas  21733  mpocnfldadd  21734  mpocnfldmul  21736  cnfldcj  21738  cnfldtset  21739  cnfldle  21740  cnfldds  21741  psrbas  22297  psrplusg  22300  psrmulr  22305  mplsubglem  22361  mplcoe1  22401  mplcoe5  22404  mdetunilem9  22990  matunitlindflem1  23049  basdif0  23326  ordtbas2  23564  ordtbas  23565  ordtopn1  23567  leordtval2  23585  iocpnfordt  23588  icomnfordt  23589  uncmp  23776  fiuncmp  23777  bwth  23783  locfincmp  23900  comppfsc  23906  1stckgenlem  23927  1stckgen  23928  ptbasin  23951  ptbasfi  23955  dfac14lem  23991  dfac14  23992  ptuncnv  24181  ptunhmeo  24182  ptcmpfi  24187  fbun  24214  trfil2  24261  ufprim  24283  ufileu  24293  filufint  24294  ufildr  24305  fmfnfm  24332  hausflim  24355  fclsfnflim  24401  alexsubALTlem4  24424  tmdgsum  24469  tsmsgsum  24513  tsmsres  24518  tsmssplit  24526  tsmsxplem1  24527  ustssco  24589  ustuqtop1  24615  prdsxmetlem  24742  prdsbl  24865  icccmplem2  25198  fsumcn  25246  cnmpopc  25304  rrxmetlem  25783  rrxmet  25784  rrxdstprj1  25785  ovolctb2  25868  ovolunnul  25876  ovolfiniun  25877  nulmbl2  25912  finiunmbl  25920  volfiniun  25923  icombl  25940  ioombl  25941  uniiccdif  25954  mbfres2  26021  itg2splitlem  26124  itg2split  26125  itgfsum  26202  itgsplit  26211  itgsplitioo  26213  dvreslem  26284  dvaddbr  26313  dvmulbr  26314  dvmptfsum  26350  lhop  26391  dvcnvrelem2  26393  mdegcl  26442  elplyr  26574  plyrem  26681  xrlimcnp  27353  fsumharmonic  27396  chtdif  27542  lgsdir2lem3  27711  lgsquadlem2  27765  dchrisum0lem1b  27899  pntrlog2bndlem6  27967  pntlemf  27989  nosupinfsep  28146  noetalem1  28155  cutsun12  28233  cofcutrtime  28370  addsuniflem  28444  addbday  28461  negsval  28468  mulsproplem12  28570  mulsproplem13  28571  mulsproplem14  28572  mulsuniflem  28592  mulsass  28609  precsexlem6  28655  precsexlem7  28656  precsexlem10  28659  precsexlem11  28660  ex-ss  31085  shsleji  32029  shsval2i  32046  ssjo  32106  sshhococi  32205  padct  33407  symgcom  33743  cycpmco2lem5  33790  cycpmco2lem6  33791  cycpmco2lem7  33792  cycpmco2  33793  gsumvsca1  33886  gsumvsca2  33887  elrgspnsubrunlem1  33907  rlocbas  33928  rlocaddval  33929  rlocmulval  33930  elrspunsn  34083  mxidlprm  34099  idlsrgbas  34140  idlsrgplusg  34141  idlsrgmulr  34143  fldextrspundgdvdslem  34423  fldextrspundgdvds  34424  constrextdg2lem  34491  esumsplit  34796  esumpad2  34799  aean  34988  sxbrsigalem2  35029  bnj931  35512  tz9.1regs  35943  subfacp1lem2b  36154  subfacp1lem3  36155  subfacp1lem5  36157  kur14lem7  36185  kur14lem9  36187  cvmliftlem10  36267  satfsschain  36337  fmlasssuc  36362  refssfne  37361  filnetlem3  37383  bj-unrab  38054  bj-snglsstag  38109  bj-2upln0  38151  bj-ccssccbar  38406  rdgssun  38569  finixpnum  38796  mbfresfi  38852  prdsbnd  38993  heibor1lem  39009  rrnequiv  39035  paddunssN  41131  sspadd1  41138  sspadd2  41139  pclfinN  41223  dochdmj1  42713  dvhdimlem  42767  elrfi  43971  mzpcompact2lem  44028  eldioph2  44039  eldioph4b  44084  ttac  44309  pwssplit4  44357  pwslnmlem2  44361  isnumbasgrplem2  44371  algbase  44437  algaddg  44438  algmulr  44439  fiuneneq  44455  idomsubgmo  44456  onexlimgt  44506  omabs2  44595  tfsconcatrnss12  44612  rclexi  44876  rtrclex  44878  trclubgNEW  44879  trclexi  44881  rtrclexi  44882  cnvrcl0  44886  cnvtrcl0  44887  dfrtrcl5  44890  trrelsuperrel2dg  44932  dfrcl2  44935  relexp0a  44977  relexpaddss  44979  trclimalb2  44987  frege83d  45009  frege131d  45025  dssmapnvod  45281  clsk3nimkb  45301  isotone1  45309  grumnudlem  45530  dmwf  46219  hfdm  46282  infxrpnf  46729  mccllem  46882  cncfiooicclem1  47176  dvmptfprod  47228  dvnprodlem1  47229  iblsplit  47249  fourierdlem54  47443  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  sge0resplit  47689  sge0split  47692  sge0splitmpt  47694  sge0xaddlem1  47716  isomenndlem  47813  hoiprodp1  47871  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvlelem4  47881  wrddun  48172  chndun  48177  chnrun  48182  dfnbgrss2  49230  gsumsplit2f  49550  linply  49713  parhomssun  51078  elpglem2  51211