Theorem ssun1 4107

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 864	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 4084	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 233	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3926	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 844   ∈ wcel 2106   ∪ cun 3886   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3433  df-un 3893  df-in 3895  df-ss 3905

This theorem is referenced by:  ssun2  4108  ssun3  4109  elun1  4111  difsssymdif  4188  inabs  4191  reuun1  4253  un00  4378  pwunss  4555  pwundif  4561  snsspr1  4749  snsstp1  4751  snsstp2  4752  uniintsn  4920  sofld  6092  sssucid  6345  fvrn0  6804  ovima0  7451  unexb  7598  dmexg  7750  suppun  7998  dftpos2  8057  tpostpos2  8061  frrlem12  8111  frrlem13  8112  wfrlem14OLD  8151  wfrlem15OLD  8152  tfrlem11  8217  oaabs2  8477  ralxpmap  8682  domss2  8921  mapunen  8931  ac6sfi  9056  frfi  9057  unfir  9080  domunfican  9085  iunfi  9105  elfiun  9187  dffi3  9188  unwdomg  9341  unxpwdom2  9345  unxpwdom  9346  cantnfp1lem1  9434  cantnfp1lem3  9436  tc2  9498  unwf  9566  rankunb  9606  r0weon  9766  infxpenlem  9767  dfac2b  9884  djudoml  9938  cdainflem  9941  infunabs  9961  infdju  9962  infdif  9963  ackbij1lem15  9988  cfsmolem  10024  isfin4p1  10069  fin23lem11  10071  fin1a2lem10  10163  fin1a2lem13  10166  axdc3lem4  10207  axcclem  10211  zornn0g  10259  ttukeylem1  10263  ttukeylem5  10267  ttukeylem7  10269  fingch  10377  fpwwe2lem12  10396  gchac  10435  wunfi  10475  wundm  10482  wunex2  10492  inar1  10529  ressxr  11017  nnssnn0  12234  un0addcl  12264  un0mulcl  12265  nn0ssxnn0  12306  hashbclem  14162  hashf1lem1  14166  hashf1lem1OLD  14167  hashf1lem2  14168  ccatrn  14292  trclublem  14704  relexpdmg  14751  relexpaddg  14762  fsumsplit  15451  fsum2d  15481  fsumabs  15511  fsumrlim  15521  fsumo1  15522  incexclem  15546  fprodsplit  15674  fprod2d  15689  lcmfunsnlem1  16340  coprmprod  16364  vdwapid1  16674  vdwlem6  16685  ramcl2  16715  isstruct2  16848  srngbase  17018  srngplusg  17019  srngmulr  17020  lmodbase  17034  lmodplusg  17035  lmodsca  17036  ipsbase  17045  ipsaddg  17046  ipsmulr  17047  phlbase  17055  phlplusg  17056  phlsca  17057  odrngbas  17112  odrngplusg  17113  odrngmulr  17114  prdssca  17165  prdsbas  17166  prdsplusg  17167  prdsmulr  17168  prdsvsca  17169  prdsip  17170  prdsle  17171  prdsds  17173  prdstset  17175  imasbas  17221  imasplusg  17226  imasmulr  17227  imassca  17228  imasvsca  17229  imasip  17230  mreexexlem2d  17352  drsdirfi  18021  ipobas  18247  ipotset  18249  acsfiindd  18269  psdmrn  18289  dirdm  18316  grpinvfval  18616  mulgfval  18700  gsumzsplit  19526  gsumsplit2  19528  gsumzunsnd  19555  gsum2dlem2  19570  dprdfadd  19621  dmdprdsplit2lem  19646  dmdprdsplit2  19647  dmdprdsplit  19648  dprdsplit  19649  ablfac1eulem  19673  lspun  20247  lspsolv  20403  lsppratlem3  20409  islbs3  20415  lbsextlem2  20419  lbsextlem4  20421  cnfldbas  20599  cnfldadd  20600  cnfldmul  20601  cnfldcj  20602  cnfldtset  20603  cnfldle  20604  cnfldds  20605  psrbagaddclOLD  21130  psrbas  21145  psrplusg  21148  psrmulr  21151  mplsubglem  21203  mplcoe1  21236  mplcoe5  21239  mdetunilem9  21767  basdif0  22101  ordtbas2  22340  ordtbas  22341  ordtopn1  22343  leordtval2  22361  iocpnfordt  22364  icomnfordt  22365  uncmp  22552  fiuncmp  22553  bwth  22559  locfincmp  22675  comppfsc  22681  1stckgenlem  22702  1stckgen  22703  ptbasin  22726  ptbasfi  22730  dfac14lem  22766  dfac14  22767  ptuncnv  22956  ptunhmeo  22957  ptcmpfi  22962  fbun  22989  trfil2  23036  ufprim  23058  ufileu  23068  filufint  23069  ufildr  23080  fmfnfm  23107  hausflim  23130  fclsfnflim  23176  alexsubALTlem4  23199  tmdgsum  23244  tsmsgsum  23288  tsmsres  23293  tsmssplit  23301  tsmsxplem1  23302  ustssco  23364  ustuqtop1  23391  prdsxmetlem  23519  prdsbl  23645  icccmplem2  23984  fsumcn  24031  cnmpopc  24089  rrxmetlem  24569  rrxmet  24570  rrxdstprj1  24571  ovolctb2  24654  ovolunnul  24662  ovolfiniun  24663  nulmbl2  24698  finiunmbl  24706  volfiniun  24709  icombl  24726  ioombl  24727  uniiccdif  24740  mbfres2  24807  itg2splitlem  24911  itg2split  24912  itgfsum  24989  itgsplit  24998  itgsplitioo  25000  dvreslem  25071  dvaddbr  25100  dvmulbr  25101  dvmptfsum  25137  lhop  25178  dvcnvrelem2  25180  mdegcl  25232  elplyr  25360  plyrem  25463  xrlimcnp  26116  fsumharmonic  26159  chtdif  26305  lgsdir2lem3  26473  lgsquadlem2  26527  dchrisum0lem1b  26661  pntrlog2bndlem6  26729  pntlemf  26751  ex-ss  28788  shsleji  29729  shsval2i  29746  ssjo  29806  sshhococi  29905  padct  31051  gsumle  31347  symgcom  31349  cycpmco2lem5  31394  cycpmco2lem6  31395  cycpmco2lem7  31396  cycpmco2  31397  gsumvsca1  31476  gsumvsca2  31477  mxidlprm  31637  idlsrgbas  31646  idlsrgplusg  31647  idlsrgmulr  31649  esumsplit  32018  esumpad2  32021  aean  32209  sxbrsigalem2  32250  bnj931  32747  subfacp1lem2b  33140  subfacp1lem3  33141  subfacp1lem5  33143  kur14lem7  33171  kur14lem9  33173  cvmliftlem10  33253  satfsschain  33323  fmlasssuc  33348  xpord2ind  33791  xpord3ind  33797  nosupinfsep  33932  noetalem1  33941  scutun12  34001  cofcutrtime  34090  negsval  34120  refssfne  34544  filnetlem3  34566  bj-unrab  35111  bj-snglsstag  35168  bj-2upln0  35210  bj-ccssccbar  35385  rdgssun  35546  finixpnum  35759  matunitlindflem1  35770  mbfresfi  35820  prdsbnd  35948  heibor1lem  35964  rrnequiv  35990  paddunssN  37819  sspadd1  37826  sspadd2  37827  pclfinN  37911  dochdmj1  39401  dvhdimlem  39455  elrfi  40513  mzpcompact2lem  40570  eldioph2  40581  eldioph4b  40630  ttac  40855  pwssplit4  40911  pwslnmlem2  40915  isnumbasgrplem2  40926  algbase  41000  algaddg  41001  algmulr  41002  fiuneneq  41019  idomsubgmo  41020  rclexi  41193  rtrclex  41195  trclubgNEW  41196  trclexi  41198  rtrclexi  41199  cnvrcl0  41203  cnvtrcl0  41204  dfrtrcl5  41207  trrelsuperrel2dg  41249  dfrcl2  41252  relexp0a  41294  relexpaddss  41296  trclimalb2  41304  frege83d  41326  frege131d  41342  dssmapnvod  41598  clsk3nimkb  41620  isotone1  41628  grumnudlem  41873  infxrpnf  42956  mccllem  43108  cncfiooicclem1  43404  dvmptfprod  43456  dvnprodlem1  43457  iblsplit  43477  fourierdlem54  43671  fourierdlem102  43719  fourierdlem103  43720  fourierdlem104  43721  fourierdlem114  43731  sge0resplit  43914  sge0split  43917  sge0splitmpt  43919  sge0xaddlem1  43941  isomenndlem  44038  hoiprodp1  44096  hoidmvlelem1  44103  hoidmvlelem2  44104  hoidmvlelem3  44105  hoidmvlelem4  44106  gsumsplit2f  45341  setrec1lem4  46363  elpglem2  46384