Theorem ssun1 4141

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

Syntax hints:   ∨ wo 847   ∈ wcel 2109   ∪ cun 3912   ⊆ wss 3914

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 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  ssun2  4142  ssun3  4143  elun1  4145  difsssymdif  4226  inabs  4229  reuun1  4291  un00  4408  pwunss  4581  pwundif  4587  snsspr1  4778  snsstp1  4780  snsstp2  4781  uniintsn  4949  sofld  6160  sssucid  6414  fvrn0  6888  f1ounsn  7247  ovima0  7568  unexb  7723  unexbOLD  7724  dmexg  7877  resf1extb  7910  xpord2indlem  8126  xpord3inddlem  8133  suppun  8163  dftpos2  8222  tpostpos2  8226  frrlem12  8276  frrlem13  8277  tfrlem11  8356  oaabs2  8613  ralxpmap  8869  domss2  9100  mapunen  9110  ac6sfi  9231  frfi  9232  unfir  9257  domunfican  9272  iunfi  9294  elfiun  9381  dffi3  9382  unwdomg  9537  unxpwdom2  9541  unxpwdom  9542  cantnfp1lem1  9631  cantnfp1lem3  9633  tc2  9695  unwf  9763  rankunb  9803  r0weon  9965  infxpenlem  9966  dfac2b  10084  djudoml  10138  cdainflem  10141  infunabs  10159  infdju  10160  infdif  10161  ackbij1lem15  10186  cfsmolem  10223  isfin4p1  10268  fin23lem11  10270  fin1a2lem10  10362  fin1a2lem13  10365  axdc3lem4  10406  axcclem  10410  zornn0g  10458  ttukeylem1  10462  ttukeylem5  10466  ttukeylem7  10468  fingch  10576  fpwwe2lem12  10595  gchac  10634  wunfi  10674  wundm  10681  wunex2  10691  inar1  10728  ressxr  11218  nnssnn0  12445  un0addcl  12475  un0mulcl  12476  nn0ssxnn0  12518  hashbclem  14417  hashf1lem1  14420  hashf1lem2  14421  ccatrn  14554  trclublem  14961  relexpdmg  15008  relexpaddg  15019  fsumsplit  15707  fsum2d  15737  fsumabs  15767  fsumrlim  15777  fsumo1  15778  incexclem  15802  fprodsplit  15932  fprod2d  15947  lcmfunsnlem1  16607  coprmprod  16631  vdwapid1  16946  vdwlem6  16957  ramcl2  16987  isstruct2  17119  srngbase  17273  srngplusg  17274  srngmulr  17275  lmodbase  17289  lmodplusg  17290  lmodsca  17291  ipsbase  17300  ipsaddg  17301  ipsmulr  17302  phlbase  17310  phlplusg  17311  phlsca  17312  odrngbas  17367  odrngplusg  17368  odrngmulr  17369  prdssca  17419  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdsip  17424  prdsle  17425  prdsds  17427  prdstset  17429  imasbas  17475  imasplusg  17480  imasmulr  17481  imassca  17482  imasvsca  17483  imasip  17484  mreexexlem2d  17606  drsdirfi  18266  ipobas  18490  ipotset  18492  acsfiindd  18512  psdmrn  18532  dirdm  18559  grpinvfval  18910  mulgfval  19001  gsumzsplit  19857  gsumsplit2  19859  gsumzunsnd  19886  gsum2dlem2  19901  dprdfadd  19952  dmdprdsplit2lem  19977  dmdprdsplit2  19978  dmdprdsplit  19979  dprdsplit  19980  ablfac1eulem  20004  lspun  20893  lspsolv  21053  lsppratlem3  21059  islbs3  21065  lbsextlem2  21069  lbsextlem4  21071  cnfldbas  21268  mpocnfldadd  21269  mpocnfldmul  21271  cnfldcj  21273  cnfldtset  21274  cnfldle  21275  cnfldds  21276  cnfldbasOLD  21283  cnfldaddOLD  21284  cnfldmulOLD  21285  cnfldcjOLD  21286  cnfldtsetOLD  21287  cnfldleOLD  21288  cnflddsOLD  21289  psrbas  21842  psrplusg  21845  psrmulr  21851  mplsubglem  21908  mplcoe1  21944  mplcoe5  21947  mdetunilem9  22507  basdif0  22840  ordtbas2  23078  ordtbas  23079  ordtopn1  23081  leordtval2  23099  iocpnfordt  23102  icomnfordt  23103  uncmp  23290  fiuncmp  23291  bwth  23297  locfincmp  23413  comppfsc  23419  1stckgenlem  23440  1stckgen  23441  ptbasin  23464  ptbasfi  23468  dfac14lem  23504  dfac14  23505  ptuncnv  23694  ptunhmeo  23695  ptcmpfi  23700  fbun  23727  trfil2  23774  ufprim  23796  ufileu  23806  filufint  23807  ufildr  23818  fmfnfm  23845  hausflim  23868  fclsfnflim  23914  alexsubALTlem4  23937  tmdgsum  23982  tsmsgsum  24026  tsmsres  24031  tsmssplit  24039  tsmsxplem1  24040  ustssco  24102  ustuqtop1  24129  prdsxmetlem  24256  prdsbl  24379  icccmplem2  24712  fsumcn  24761  cnmpopc  24822  rrxmetlem  25307  rrxmet  25308  rrxdstprj1  25309  ovolctb2  25393  ovolunnul  25401  ovolfiniun  25402  nulmbl2  25437  finiunmbl  25445  volfiniun  25448  icombl  25465  ioombl  25466  uniiccdif  25479  mbfres2  25546  itg2splitlem  25649  itg2split  25650  itgfsum  25728  itgsplit  25737  itgsplitioo  25739  dvreslem  25810  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvmptfsum  25879  lhop  25921  dvcnvrelem2  25923  mdegcl  25974  elplyr  26106  plyrem  26213  xrlimcnp  26878  fsumharmonic  26922  chtdif  27068  lgsdir2lem3  27238  lgsquadlem2  27292  dchrisum0lem1b  27426  pntrlog2bndlem6  27494  pntlemf  27516  nosupinfsep  27644  noetalem1  27653  scutun12  27722  cofcutrtime  27835  addsuniflem  27908  addsbday  27924  negsval  27931  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  mulsuniflem  28052  mulsass  28069  precsexlem6  28114  precsexlem7  28115  precsexlem10  28118  precsexlem11  28119  ex-ss  30356  shsleji  31299  shsval2i  31316  ssjo  31376  sshhococi  31475  padct  32643  gsumle  33038  symgcom  33040  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  gsumvsca1  33179  gsumvsca2  33180  elrgspnsubrunlem1  33198  rlocbas  33218  rlocaddval  33219  rlocmulval  33220  elrspunsn  33400  mxidlprm  33441  idlsrgbas  33475  idlsrgplusg  33476  idlsrgmulr  33478  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  constrextdg2lem  33738  esumsplit  34043  esumpad2  34046  aean  34234  sxbrsigalem2  34277  bnj931  34760  subfacp1lem2b  35168  subfacp1lem3  35169  subfacp1lem5  35171  kur14lem7  35199  kur14lem9  35201  cvmliftlem10  35281  satfsschain  35351  fmlasssuc  35376  refssfne  36346  filnetlem3  36368  bj-unrab  36914  bj-snglsstag  36969  bj-2upln0  37011  bj-ccssccbar  37205  rdgssun  37366  finixpnum  37599  matunitlindflem1  37610  mbfresfi  37660  prdsbnd  37787  heibor1lem  37803  rrnequiv  37829  paddunssN  39802  sspadd1  39809  sspadd2  39810  pclfinN  39894  dochdmj1  41384  dvhdimlem  41438  elrfi  42682  mzpcompact2lem  42739  eldioph2  42750  eldioph4b  42799  ttac  43025  pwssplit4  43078  pwslnmlem2  43082  isnumbasgrplem2  43093  algbase  43163  algaddg  43164  algmulr  43165  fiuneneq  43181  idomsubgmo  43182  onexlimgt  43232  omabs2  43321  tfsconcatrnss12  43338  rclexi  43604  rtrclex  43606  trclubgNEW  43607  trclexi  43609  rtrclexi  43610  cnvrcl0  43614  cnvtrcl0  43615  dfrtrcl5  43618  trrelsuperrel2dg  43660  dfrcl2  43663  relexp0a  43705  relexpaddss  43707  trclimalb2  43715  frege83d  43737  frege131d  43753  dssmapnvod  44009  clsk3nimkb  44029  isotone1  44037  grumnudlem  44274  dmwf  44955  infxrpnf  45442  mccllem  45595  cncfiooicclem1  45891  dvmptfprod  45943  dvnprodlem1  45944  iblsplit  45964  fourierdlem54  46158  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  sge0resplit  46404  sge0split  46407  sge0splitmpt  46409  sge0xaddlem1  46431  isomenndlem  46528  hoiprodp1  46586  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  dfnbgrss2  47859  gsumsplit2f  48168  setrec1lem4  49679  elpglem2  49701