Theorem ssun1 4132

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

Syntax hints:   ∨ wo 848   ∈ wcel 2114   ∪ cun 3901   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  ssun2  4133  ssun3  4134  elun1  4136  difsssymdif  4217  inabs  4220  reuun1  4282  un00  4399  pwunss  4574  pwundif  4580  snsspr1  4772  snsstp1  4774  snsstp2  4775  uniintsn  4942  sofld  6153  sssucid  6407  fvrn0  6870  f1ounsn  7228  ovima0  7547  unexb  7702  unexbOLD  7703  dmexg  7853  resf1extb  7886  xpord2indlem  8099  xpord3inddlem  8106  suppun  8136  dftpos2  8195  tpostpos2  8199  frrlem12  8249  frrlem13  8250  tfrlem11  8329  oaabs2  8587  ralxpmap  8846  domss2  9076  mapunen  9086  ac6sfi  9196  frfi  9197  unfir  9220  domunfican  9234  iunfi  9255  elfiun  9345  dffi3  9346  unwdomg  9501  unxpwdom2  9505  unxpwdom  9506  cantnfp1lem1  9599  cantnfp1lem3  9601  tc2  9661  unwf  9734  rankunb  9774  r0weon  9934  infxpenlem  9935  dfac2b  10053  djudoml  10107  cdainflem  10110  infunabs  10128  infdju  10129  infdif  10130  ackbij1lem15  10155  cfsmolem  10192  isfin4p1  10237  fin23lem11  10239  fin1a2lem10  10331  fin1a2lem13  10334  axdc3lem4  10375  axcclem  10379  zornn0g  10427  ttukeylem1  10431  ttukeylem5  10435  ttukeylem7  10437  fingch  10546  fpwwe2lem12  10565  gchac  10604  wunfi  10644  wundm  10651  wunex2  10661  inar1  10698  ressxr  11188  nnssnn0  12416  un0addcl  12446  un0mulcl  12447  nn0ssxnn0  12489  hashbclem  14387  hashf1lem1  14390  hashf1lem2  14391  ccatrn  14525  trclublem  14930  relexpdmg  14977  relexpaddg  14988  fsumsplit  15676  fsum2d  15706  fsumabs  15736  fsumrlim  15746  fsumo1  15747  incexclem  15771  fprodsplit  15901  fprod2d  15916  lcmfunsnlem1  16576  coprmprod  16600  vdwapid1  16915  vdwlem6  16926  ramcl2  16956  isstruct2  17088  srngbase  17242  srngplusg  17243  srngmulr  17244  lmodbase  17258  lmodplusg  17259  lmodsca  17260  ipsbase  17269  ipsaddg  17270  ipsmulr  17271  phlbase  17279  phlplusg  17280  phlsca  17281  odrngbas  17336  odrngplusg  17337  odrngmulr  17338  prdssca  17388  prdsbas  17389  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdsip  17393  prdsle  17394  prdsds  17396  prdstset  17398  imasbas  17445  imasplusg  17450  imasmulr  17451  imassca  17452  imasvsca  17453  imasip  17454  mreexexlem2d  17580  drsdirfi  18240  ipobas  18466  ipotset  18468  acsfiindd  18488  psdmrn  18508  dirdm  18535  grpinvfval  18920  mulgfval  19011  gsumzsplit  19868  gsumsplit2  19870  gsumzunsnd  19897  gsum2dlem2  19912  dprdfadd  19963  dmdprdsplit2lem  19988  dmdprdsplit2  19989  dmdprdsplit  19990  dprdsplit  19991  ablfac1eulem  20015  gsumle  20086  lspun  20950  lspsolv  21110  lsppratlem3  21116  islbs3  21122  lbsextlem2  21126  lbsextlem4  21128  cnfldbas  21325  mpocnfldadd  21326  mpocnfldmul  21328  cnfldcj  21330  cnfldtset  21331  cnfldle  21332  cnfldds  21333  cnfldbasOLD  21340  cnfldaddOLD  21341  cnfldmulOLD  21342  cnfldcjOLD  21343  cnfldtsetOLD  21344  cnfldleOLD  21345  cnflddsOLD  21346  psrbas  21901  psrplusg  21904  psrmulr  21910  mplsubglem  21966  mplcoe1  22004  mplcoe5  22007  mdetunilem9  22576  basdif0  22909  ordtbas2  23147  ordtbas  23148  ordtopn1  23150  leordtval2  23168  iocpnfordt  23171  icomnfordt  23172  uncmp  23359  fiuncmp  23360  bwth  23366  locfincmp  23482  comppfsc  23488  1stckgenlem  23509  1stckgen  23510  ptbasin  23533  ptbasfi  23537  dfac14lem  23573  dfac14  23574  ptuncnv  23763  ptunhmeo  23764  ptcmpfi  23769  fbun  23796  trfil2  23843  ufprim  23865  ufileu  23875  filufint  23876  ufildr  23887  fmfnfm  23914  hausflim  23937  fclsfnflim  23983  alexsubALTlem4  24006  tmdgsum  24051  tsmsgsum  24095  tsmsres  24100  tsmssplit  24108  tsmsxplem1  24109  ustssco  24171  ustuqtop1  24197  prdsxmetlem  24324  prdsbl  24447  icccmplem2  24780  fsumcn  24829  cnmpopc  24890  rrxmetlem  25375  rrxmet  25376  rrxdstprj1  25377  ovolctb2  25461  ovolunnul  25469  ovolfiniun  25470  nulmbl2  25505  finiunmbl  25513  volfiniun  25516  icombl  25533  ioombl  25534  uniiccdif  25547  mbfres2  25614  itg2splitlem  25717  itg2split  25718  itgfsum  25796  itgsplit  25805  itgsplitioo  25807  dvreslem  25878  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvmptfsum  25947  lhop  25989  dvcnvrelem2  25991  mdegcl  26042  elplyr  26174  plyrem  26281  xrlimcnp  26946  fsumharmonic  26990  chtdif  27136  lgsdir2lem3  27306  lgsquadlem2  27360  dchrisum0lem1b  27494  pntrlog2bndlem6  27562  pntlemf  27584  nosupinfsep  27712  noetalem1  27721  cutsun12  27798  cofcutrtime  27935  addsuniflem  28009  addbday  28026  negsval  28033  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  mulsuniflem  28157  mulsass  28174  precsexlem6  28220  precsexlem7  28221  precsexlem10  28224  precsexlem11  28225  ex-ss  30514  shsleji  31458  shsval2i  31475  ssjo  31535  sshhococi  31634  padct  32808  symgcom  33177  cycpmco2lem5  33224  cycpmco2lem6  33225  cycpmco2lem7  33226  cycpmco2  33227  gsumvsca1  33320  gsumvsca2  33321  elrgspnsubrunlem1  33341  rlocbas  33361  rlocaddval  33362  rlocmulval  33363  elrspunsn  33522  mxidlprm  33563  idlsrgbas  33597  idlsrgplusg  33598  idlsrgmulr  33600  fldextrspundgdvdslem  33858  fldextrspundgdvds  33859  constrextdg2lem  33926  esumsplit  34231  esumpad2  34234  aean  34422  sxbrsigalem2  34464  bnj931  34947  tz9.1regs  35312  subfacp1lem2b  35397  subfacp1lem3  35398  subfacp1lem5  35400  kur14lem7  35428  kur14lem9  35430  cvmliftlem10  35510  satfsschain  35580  fmlasssuc  35605  refssfne  36574  filnetlem3  36596  bj-unrab  37174  bj-snglsstag  37229  bj-2upln0  37271  bj-ccssccbar  37472  rdgssun  37633  finixpnum  37856  matunitlindflem1  37867  mbfresfi  37917  prdsbnd  38044  heibor1lem  38060  rrnequiv  38086  paddunssN  40184  sspadd1  40191  sspadd2  40192  pclfinN  40276  dochdmj1  41766  dvhdimlem  41820  elrfi  43051  mzpcompact2lem  43108  eldioph2  43119  eldioph4b  43168  ttac  43393  pwssplit4  43446  pwslnmlem2  43450  isnumbasgrplem2  43461  algbase  43531  algaddg  43532  algmulr  43533  fiuneneq  43549  idomsubgmo  43550  onexlimgt  43600  omabs2  43689  tfsconcatrnss12  43706  rclexi  43971  rtrclex  43973  trclubgNEW  43974  trclexi  43976  rtrclexi  43977  cnvrcl0  43981  cnvtrcl0  43982  dfrtrcl5  43985  trrelsuperrel2dg  44027  dfrcl2  44030  relexp0a  44072  relexpaddss  44074  trclimalb2  44082  frege83d  44104  frege131d  44120  dssmapnvod  44376  clsk3nimkb  44396  isotone1  44404  grumnudlem  44641  dmwf  45321  infxrpnf  45804  mccllem  45957  cncfiooicclem1  46251  dvmptfprod  46303  dvnprodlem1  46304  iblsplit  46324  fourierdlem54  46518  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem114  46578  sge0resplit  46764  sge0split  46767  sge0splitmpt  46769  sge0xaddlem1  46791  isomenndlem  46888  hoiprodp1  46946  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem4  46956  dfnbgrss2  48219  gsumsplit2f  48540  setrec1lem4  50049  elpglem2  50071