Theorem ssun1 4146

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 863	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 4123	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 236	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3969	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 843   ∈ wcel 2108   ∪ cun 3932   ⊆ wss 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-un 3939  df-in 3941  df-ss 3950

This theorem is referenced by:  ssun2  4147  ssun3  4148  elun1  4150  difsssymdif  4227  inabs  4230  reuun1  4283  un00  4392  snsspr1  4739  snsstp1  4741  snsstp2  4742  uniintsn  4904  pwunss  5446  pwundif  5449  sofld  6037  sssucid  6261  fvrn0  6691  ovima0  7319  unexb  7463  dmexg  7605  suppun  7842  dftpos2  7901  tpostpos2  7905  wfrlem14  7960  wfrlem15  7961  tfrlem11  8016  oaabs2  8264  ralxpmap  8452  domss2  8668  mapunen  8678  ac6sfi  8754  frfi  8755  unfir  8778  domunfican  8783  iunfi  8804  elfiun  8886  dffi3  8887  unwdomg  9040  unxpwdom2  9044  unxpwdom  9045  cantnfp1lem1  9133  cantnfp1lem3  9135  tc2  9176  unwf  9231  rankunb  9271  r0weon  9430  infxpenlem  9431  dfac2b  9548  djudoml  9602  cdainflem  9605  infunabs  9621  infdju  9622  infdif  9623  ackbij1lem15  9648  cfsmolem  9684  isfin4p1  9729  fin23lem11  9731  fin1a2lem10  9823  fin1a2lem13  9826  axdc3lem4  9867  axcclem  9871  zornn0g  9919  ttukeylem1  9923  ttukeylem5  9927  ttukeylem7  9929  fingch  10037  fpwwe2lem13  10056  gchac  10095  wunfi  10135  wundm  10142  wunex2  10152  inar1  10189  ressxr  10677  nnssnn0  11892  un0addcl  11922  un0mulcl  11923  nn0ssxnn0  11962  hashbclem  13802  hashf1lem1  13805  hashf1lem2  13806  ccatrn  13935  trclublem  14347  relexpdmg  14393  relexpaddg  14404  fsumsplit  15089  fsum2d  15118  fsumabs  15148  fsumrlim  15158  fsumo1  15159  incexclem  15183  fprodsplit  15312  fprod2d  15327  lcmfunsnlem1  15973  coprmprod  15997  vdwapid1  16303  vdwlem6  16314  ramcl2  16344  isstruct2  16485  srngbase  16620  srngplusg  16621  srngmulr  16622  lmodbase  16629  lmodplusg  16630  lmodsca  16631  ipsbase  16636  ipsaddg  16637  ipsmulr  16638  phlbase  16646  phlplusg  16647  phlsca  16648  odrngbas  16672  odrngplusg  16673  odrngmulr  16674  prdssca  16721  prdsbas  16722  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  prdsip  16726  prdsle  16727  prdsds  16729  prdstset  16731  imasbas  16777  imasplusg  16782  imasmulr  16783  imassca  16784  imasvsca  16785  imasip  16786  mreexexlem2d  16908  drsdirfi  17540  ipobas  17757  ipotset  17759  acsfiindd  17779  psdmrn  17809  dirdm  17836  grpinvfval  18134  mulgfval  18218  gsumzsplit  19039  gsumsplit2  19041  gsumzunsnd  19068  gsum2dlem2  19083  dprdfadd  19134  dmdprdsplit2lem  19159  dmdprdsplit2  19160  dmdprdsplit  19161  dprdsplit  19162  ablfac1eulem  19186  lspun  19751  lspsolv  19907  lsppratlem3  19913  islbs3  19919  lbsextlem2  19923  lbsextlem4  19925  psrbagaddcl  20142  psrbas  20150  psrplusg  20153  psrmulr  20156  mplsubglem  20206  mplcoe1  20238  mplcoe5  20241  cnfldbas  20541  cnfldadd  20542  cnfldmul  20543  cnfldcj  20544  cnfldtset  20545  cnfldle  20546  cnfldds  20547  mdetunilem9  21221  basdif0  21553  ordtbas2  21791  ordtbas  21792  ordtopn1  21794  leordtval2  21812  iocpnfordt  21815  icomnfordt  21816  uncmp  22003  fiuncmp  22004  bwth  22010  locfincmp  22126  comppfsc  22132  1stckgenlem  22153  1stckgen  22154  ptbasin  22177  ptbasfi  22181  dfac14lem  22217  dfac14  22218  ptuncnv  22407  ptunhmeo  22408  ptcmpfi  22413  fbun  22440  trfil2  22487  ufprim  22509  ufileu  22519  filufint  22520  ufildr  22531  fmfnfm  22558  hausflim  22581  fclsfnflim  22627  alexsubALTlem4  22650  tmdgsum  22695  tsmsgsum  22739  tsmsres  22744  tsmssplit  22752  tsmsxplem1  22753  ustssco  22815  ustuqtop1  22842  prdsxmetlem  22970  prdsbl  23093  icccmplem2  23423  fsumcn  23470  cnmpopc  23524  rrxmetlem  24002  rrxmet  24003  rrxdstprj1  24004  ovolctb2  24085  ovolunnul  24093  ovolfiniun  24094  nulmbl2  24129  finiunmbl  24137  volfiniun  24140  icombl  24157  ioombl  24158  uniiccdif  24171  mbfres2  24238  itg2splitlem  24341  itg2split  24342  itgfsum  24419  itgsplit  24428  itgsplitioo  24430  dvreslem  24499  dvaddbr  24527  dvmulbr  24528  dvmptfsum  24564  lhop  24605  dvcnvrelem2  24607  mdegcl  24655  elplyr  24783  plyrem  24886  xrlimcnp  25538  fsumharmonic  25581  chtdif  25727  lgsdir2lem3  25895  lgsquadlem2  25949  dchrisum0lem1b  26083  pntrlog2bndlem6  26151  pntlemf  26173  ex-ss  28198  shsleji  29139  shsval2i  29156  ssjo  29216  sshhococi  29315  padct  30447  gsumle  30718  symgcom  30720  cycpmco2lem5  30765  cycpmco2lem6  30766  cycpmco2lem7  30767  cycpmco2  30768  gsumvsca1  30847  gsumvsca2  30848  mxidlprm  30970  esumsplit  31305  esumpad2  31308  aean  31496  sxbrsigalem2  31537  bnj931  32035  subfacp1lem2b  32421  subfacp1lem3  32422  subfacp1lem5  32424  kur14lem7  32452  kur14lem9  32454  cvmliftlem10  32534  satfsschain  32604  fmlasssuc  32629  dftrpred3g  33065  frrlem12  33127  frrlem13  33128  scutun12  33264  refssfne  33699  filnetlem3  33721  bj-unrab  34237  bj-snglsstag  34286  bj-2upln0  34328  bj-ccssccbar  34491  rdgssun  34651  finixpnum  34869  matunitlindflem1  34880  mbfresfi  34930  prdsbnd  35063  heibor1lem  35079  rrnequiv  35105  paddunssN  36936  sspadd1  36943  sspadd2  36944  pclfinN  37028  dochdmj1  38518  dvhdimlem  38572  elrfi  39281  mzpcompact2lem  39338  eldioph2  39349  eldioph4b  39398  ttac  39623  pwssplit4  39679  pwslnmlem2  39683  isnumbasgrplem2  39694  algbase  39768  algaddg  39769  algmulr  39770  fiuneneq  39787  idomsubgmo  39788  rclexi  39965  rtrclex  39967  trclubgNEW  39968  trclexi  39970  rtrclexi  39971  cnvrcl0  39975  cnvtrcl0  39976  dfrtrcl5  39979  trrelsuperrel2dg  40006  dfrcl2  40009  relexp0a  40051  relexpaddss  40053  trclimalb2  40061  frege83d  40083  frege131d  40099  dssmapnvod  40356  clsk3nimkb  40380  isotone1  40388  grumnudlem  40611  infxrpnf  41710  mccllem  41867  cncfiooicclem1  42165  dvmptfprod  42219  dvnprodlem1  42220  iblsplit  42240  fourierdlem54  42435  fourierdlem102  42483  fourierdlem103  42484  fourierdlem104  42485  fourierdlem114  42495  sge0resplit  42678  sge0split  42681  sge0splitmpt  42683  sge0xaddlem1  42705  isomenndlem  42802  hoiprodp1  42860  hoidmvlelem1  42867  hoidmvlelem2  42868  hoidmvlelem3  42869  hoidmvlelem4  42870  gsumsplit2f  44077  setrec1lem4  44783  elpglem2  44804