Theorem ssun1 4137

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

Syntax hints:   ∨ wo 847   ∈ wcel 2109   ∪ cun 3909   ⊆ wss 3911

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 3446  df-un 3916  df-ss 3928

This theorem is referenced by:  ssun2  4138  ssun3  4139  elun1  4141  difsssymdif  4222  inabs  4225  reuun1  4287  un00  4404  pwunss  4577  pwundif  4583  snsspr1  4774  snsstp1  4776  snsstp2  4777  uniintsn  4945  sofld  6148  sssucid  6402  fvrn0  6870  f1ounsn  7229  ovima0  7548  unexb  7703  unexbOLD  7704  dmexg  7857  resf1extb  7890  xpord2indlem  8103  xpord3inddlem  8110  suppun  8140  dftpos2  8199  tpostpos2  8203  frrlem12  8253  frrlem13  8254  tfrlem11  8333  oaabs2  8590  ralxpmap  8846  domss2  9077  mapunen  9087  ac6sfi  9207  frfi  9208  unfir  9233  domunfican  9248  iunfi  9270  elfiun  9357  dffi3  9358  unwdomg  9513  unxpwdom2  9517  unxpwdom  9518  cantnfp1lem1  9607  cantnfp1lem3  9609  tc2  9671  unwf  9739  rankunb  9779  r0weon  9941  infxpenlem  9942  dfac2b  10060  djudoml  10114  cdainflem  10117  infunabs  10135  infdju  10136  infdif  10137  ackbij1lem15  10162  cfsmolem  10199  isfin4p1  10244  fin23lem11  10246  fin1a2lem10  10338  fin1a2lem13  10341  axdc3lem4  10382  axcclem  10386  zornn0g  10434  ttukeylem1  10438  ttukeylem5  10442  ttukeylem7  10444  fingch  10552  fpwwe2lem12  10571  gchac  10610  wunfi  10650  wundm  10657  wunex2  10667  inar1  10704  ressxr  11194  nnssnn0  12421  un0addcl  12451  un0mulcl  12452  nn0ssxnn0  12494  hashbclem  14393  hashf1lem1  14396  hashf1lem2  14397  ccatrn  14530  trclublem  14937  relexpdmg  14984  relexpaddg  14995  fsumsplit  15683  fsum2d  15713  fsumabs  15743  fsumrlim  15753  fsumo1  15754  incexclem  15778  fprodsplit  15908  fprod2d  15923  lcmfunsnlem1  16583  coprmprod  16607  vdwapid1  16922  vdwlem6  16933  ramcl2  16963  isstruct2  17095  srngbase  17249  srngplusg  17250  srngmulr  17251  lmodbase  17265  lmodplusg  17266  lmodsca  17267  ipsbase  17276  ipsaddg  17277  ipsmulr  17278  phlbase  17286  phlplusg  17287  phlsca  17288  odrngbas  17343  odrngplusg  17344  odrngmulr  17345  prdssca  17395  prdsbas  17396  prdsplusg  17397  prdsmulr  17398  prdsvsca  17399  prdsip  17400  prdsle  17401  prdsds  17403  prdstset  17405  imasbas  17451  imasplusg  17456  imasmulr  17457  imassca  17458  imasvsca  17459  imasip  17460  mreexexlem2d  17582  drsdirfi  18242  ipobas  18466  ipotset  18468  acsfiindd  18488  psdmrn  18508  dirdm  18535  grpinvfval  18886  mulgfval  18977  gsumzsplit  19833  gsumsplit2  19835  gsumzunsnd  19862  gsum2dlem2  19877  dprdfadd  19928  dmdprdsplit2lem  19953  dmdprdsplit2  19954  dmdprdsplit  19955  dprdsplit  19956  ablfac1eulem  19980  lspun  20869  lspsolv  21029  lsppratlem3  21035  islbs3  21041  lbsextlem2  21045  lbsextlem4  21047  cnfldbas  21244  mpocnfldadd  21245  mpocnfldmul  21247  cnfldcj  21249  cnfldtset  21250  cnfldle  21251  cnfldds  21252  cnfldbasOLD  21259  cnfldaddOLD  21260  cnfldmulOLD  21261  cnfldcjOLD  21262  cnfldtsetOLD  21263  cnfldleOLD  21264  cnflddsOLD  21265  psrbas  21818  psrplusg  21821  psrmulr  21827  mplsubglem  21884  mplcoe1  21920  mplcoe5  21923  mdetunilem9  22483  basdif0  22816  ordtbas2  23054  ordtbas  23055  ordtopn1  23057  leordtval2  23075  iocpnfordt  23078  icomnfordt  23079  uncmp  23266  fiuncmp  23267  bwth  23273  locfincmp  23389  comppfsc  23395  1stckgenlem  23416  1stckgen  23417  ptbasin  23440  ptbasfi  23444  dfac14lem  23480  dfac14  23481  ptuncnv  23670  ptunhmeo  23671  ptcmpfi  23676  fbun  23703  trfil2  23750  ufprim  23772  ufileu  23782  filufint  23783  ufildr  23794  fmfnfm  23821  hausflim  23844  fclsfnflim  23890  alexsubALTlem4  23913  tmdgsum  23958  tsmsgsum  24002  tsmsres  24007  tsmssplit  24015  tsmsxplem1  24016  ustssco  24078  ustuqtop1  24105  prdsxmetlem  24232  prdsbl  24355  icccmplem2  24688  fsumcn  24737  cnmpopc  24798  rrxmetlem  25283  rrxmet  25284  rrxdstprj1  25285  ovolctb2  25369  ovolunnul  25377  ovolfiniun  25378  nulmbl2  25413  finiunmbl  25421  volfiniun  25424  icombl  25441  ioombl  25442  uniiccdif  25455  mbfres2  25522  itg2splitlem  25625  itg2split  25626  itgfsum  25704  itgsplit  25713  itgsplitioo  25715  dvreslem  25786  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  dvmptfsum  25855  lhop  25897  dvcnvrelem2  25899  mdegcl  25950  elplyr  26082  plyrem  26189  xrlimcnp  26854  fsumharmonic  26898  chtdif  27044  lgsdir2lem3  27214  lgsquadlem2  27268  dchrisum0lem1b  27402  pntrlog2bndlem6  27470  pntlemf  27492  nosupinfsep  27620  noetalem1  27629  scutun12  27698  cofcutrtime  27811  addsuniflem  27884  addsbday  27900  negsval  27907  mulsproplem12  28006  mulsproplem13  28007  mulsproplem14  28008  mulsuniflem  28028  mulsass  28045  precsexlem6  28090  precsexlem7  28091  precsexlem10  28094  precsexlem11  28095  ex-ss  30329  shsleji  31272  shsval2i  31289  ssjo  31349  sshhococi  31448  padct  32616  gsumle  33011  symgcom  33013  cycpmco2lem5  33060  cycpmco2lem6  33061  cycpmco2lem7  33062  cycpmco2  33063  gsumvsca1  33152  gsumvsca2  33153  elrgspnsubrunlem1  33171  rlocbas  33191  rlocaddval  33192  rlocmulval  33193  elrspunsn  33373  mxidlprm  33414  idlsrgbas  33448  idlsrgplusg  33449  idlsrgmulr  33451  fldextrspundgdvdslem  33648  fldextrspundgdvds  33649  constrextdg2lem  33711  esumsplit  34016  esumpad2  34019  aean  34207  sxbrsigalem2  34250  bnj931  34733  subfacp1lem2b  35141  subfacp1lem3  35142  subfacp1lem5  35144  kur14lem7  35172  kur14lem9  35174  cvmliftlem10  35254  satfsschain  35324  fmlasssuc  35349  refssfne  36319  filnetlem3  36341  bj-unrab  36887  bj-snglsstag  36942  bj-2upln0  36984  bj-ccssccbar  37178  rdgssun  37339  finixpnum  37572  matunitlindflem1  37583  mbfresfi  37633  prdsbnd  37760  heibor1lem  37776  rrnequiv  37802  paddunssN  39775  sspadd1  39782  sspadd2  39783  pclfinN  39867  dochdmj1  41357  dvhdimlem  41411  elrfi  42655  mzpcompact2lem  42712  eldioph2  42723  eldioph4b  42772  ttac  42998  pwssplit4  43051  pwslnmlem2  43055  isnumbasgrplem2  43066  algbase  43136  algaddg  43137  algmulr  43138  fiuneneq  43154  idomsubgmo  43155  onexlimgt  43205  omabs2  43294  tfsconcatrnss12  43311  rclexi  43577  rtrclex  43579  trclubgNEW  43580  trclexi  43582  rtrclexi  43583  cnvrcl0  43587  cnvtrcl0  43588  dfrtrcl5  43591  trrelsuperrel2dg  43633  dfrcl2  43636  relexp0a  43678  relexpaddss  43680  trclimalb2  43688  frege83d  43710  frege131d  43726  dssmapnvod  43982  clsk3nimkb  44002  isotone1  44010  grumnudlem  44247  dmwf  44928  infxrpnf  45415  mccllem  45568  cncfiooicclem1  45864  dvmptfprod  45916  dvnprodlem1  45917  iblsplit  45937  fourierdlem54  46131  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem114  46191  sge0resplit  46377  sge0split  46380  sge0splitmpt  46382  sge0xaddlem1  46404  isomenndlem  46501  hoiprodp1  46559  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem4  46569  dfnbgrss2  47832  gsumsplit2f  48141  setrec1lem4  49652  elpglem2  49674