Theorem ssun1 4131

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

Syntax hints:   ∨ wo 860   ∈ wcel 2143   ∪ cun 3903   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922

This theorem is referenced by:  ssun2  4132  ssun3  4133  elun1  4135  difsssymdif  4216  inabs  4219  reuun1  4281  un00  4364  pwunss  4580  pwundif  4587  snsspr1  4780  snsstp1  4782  snsstp2  4783  uniintsn  4950  sofld  6185  sssucid  6443  fvrn0  6909  f1ounsn  7270  ovima0  7589  unexb  7744  dmexg  7894  resf1extb  7927  xpord2indlem  8139  xpord3inddlem  8146  suppun  8176  dftpos2  8235  tpostpos2  8239  frrlem12  8290  frrlem13  8291  tfrlem11  8371  oaabs2  8631  ralxpmap  8890  domss2  9120  mapunen  9130  ac6sfi  9240  frfi  9241  unfir  9264  domunfican  9277  iunfi  9296  elfiun  9386  dffi3  9387  unwdomg  9542  unxpwdom2  9546  unxpwdom  9547  cantnfp1lem1  9643  cantnfp1lem3  9645  tc2  9705  unwf  9778  rankunb  9818  r0weon  9992  infxpenlem  9993  dfac2b  10110  djudoml  10164  cdainflem  10167  infunabs  10185  infdju  10186  infdif  10187  ackbij1lem15  10212  cfsmolem  10249  isfin4p1  10294  fin23lem11  10296  fin1a2lem10  10388  fin1a2lem13  10391  axdc3lem4  10432  axcclem  10436  zornn0g  10484  ttukeylem1  10488  ttukeylem5  10492  ttukeylem7  10494  fingch  10603  fpwwe2lem12  10622  gchac  10661  wunfi  10701  wundm  10708  wunex2  10718  inar1  10755  ressxr  11248  nnssnn0  12502  un0addcl  12532  un0mulcl  12533  nn0ssxnn0  12575  hashbclem  14485  hashf1lem1  14488  hashf1lem2  14489  ccatrn  14623  trclublem  15028  relexpdmg  15075  relexpaddg  15086  fsumsplit  15788  fsum2d  15818  fsumabs  15849  fsumrlim  15859  fsumo1  15860  incexclem  15886  fprodsplit  16016  fprod2d  16031  lcmfunsnlem1  16690  coprmprod  16714  vdwapid1  17030  vdwlem6  17041  ramcl2  17071  isstruct2  17204  srngbase  17358  srngplusg  17359  srngmulr  17360  lmodbase  17374  lmodplusg  17375  lmodsca  17376  ipsbase  17385  ipsaddg  17386  ipsmulr  17387  phlbase  17395  phlplusg  17396  phlsca  17397  odrngbas  17452  odrngplusg  17453  odrngmulr  17454  prdssca  17504  prdsbas  17505  prdsplusg  17506  prdsmulr  17507  prdsvsca  17508  prdsip  17509  prdsle  17510  prdsds  17512  prdstset  17514  imasbas  17561  imasplusg  17566  imasmulr  17567  imassca  17568  imasvsca  17569  imasip  17570  mreexexlem2d  17696  drsdirfi  18356  ipobas  18582  ipotset  18584  acsfiindd  18604  psdmrn  18624  dirdm  18651  grpinvfval  19040  mulgfval  19130  gsumzsplit  19992  gsumsplit2  19994  gsumzunsnd  20021  gsum2dlem2  20036  dprdfadd  20087  dmdprdsplit2lem  20112  dmdprdsplit2  20113  dmdprdsplit  20114  dprdsplit  20115  ablfac1eulem  20139  gsumle  20210  lspun  21108  lspsolv  21267  lsppratlem3  21273  islbs3  21279  lbsextlem2  21283  lbsextlem4  21285  cnfldbas  21526  mpocnfldadd  21527  mpocnfldmul  21529  cnfldcj  21531  cnfldtset  21532  cnfldle  21533  cnfldds  21534  psrbas  22084  psrplusg  22087  psrmulr  22092  mplsubglem  22148  mplcoe1  22188  mplcoe5  22191  mdetunilem9  22777  basdif0  23110  ordtbas2  23348  ordtbas  23349  ordtopn1  23351  leordtval2  23369  iocpnfordt  23372  icomnfordt  23373  uncmp  23560  fiuncmp  23561  bwth  23567  locfincmp  23683  comppfsc  23689  1stckgenlem  23710  1stckgen  23711  ptbasin  23734  ptbasfi  23738  dfac14lem  23774  dfac14  23775  ptuncnv  23964  ptunhmeo  23965  ptcmpfi  23970  fbun  23997  trfil2  24044  ufprim  24066  ufileu  24076  filufint  24077  ufildr  24088  fmfnfm  24115  hausflim  24138  fclsfnflim  24184  alexsubALTlem4  24207  tmdgsum  24252  tsmsgsum  24296  tsmsres  24301  tsmssplit  24309  tsmsxplem1  24310  ustssco  24372  ustuqtop1  24398  prdsxmetlem  24525  prdsbl  24648  icccmplem2  24981  fsumcn  25029  cnmpopc  25087  rrxmetlem  25566  rrxmet  25567  rrxdstprj1  25568  ovolctb2  25651  ovolunnul  25659  ovolfiniun  25660  nulmbl2  25695  finiunmbl  25703  volfiniun  25706  icombl  25723  ioombl  25724  uniiccdif  25737  mbfres2  25804  itg2splitlem  25907  itg2split  25908  itgfsum  25986  itgsplit  25995  itgsplitioo  25997  dvreslem  26068  dvaddbr  26097  dvmulbr  26098  dvmptfsum  26134  lhop  26175  dvcnvrelem2  26177  mdegcl  26226  elplyr  26358  plyrem  26466  xrlimcnp  27133  fsumharmonic  27176  chtdif  27322  lgsdir2lem3  27491  lgsquadlem2  27545  dchrisum0lem1b  27679  pntrlog2bndlem6  27747  pntlemf  27769  nosupinfsep  27896  noetalem1  27905  cutsun12  27983  cofcutrtime  28120  addsuniflem  28194  addbday  28211  negsval  28218  mulsproplem12  28320  mulsproplem13  28321  mulsproplem14  28322  mulsuniflem  28342  mulsass  28359  precsexlem6  28405  precsexlem7  28406  precsexlem10  28409  precsexlem11  28410  ex-ss  30778  shsleji  31722  shsval2i  31739  ssjo  31799  sshhococi  31898  padct  33063  symgcom  33403  cycpmco2lem5  33450  cycpmco2lem6  33451  cycpmco2lem7  33452  cycpmco2  33453  gsumvsca1  33546  gsumvsca2  33547  elrgspnsubrunlem1  33567  rlocbas  33588  rlocaddval  33589  rlocmulval  33590  elrspunsn  33737  mxidlprm  33753  idlsrgbas  33794  idlsrgplusg  33795  idlsrgmulr  33797  fldextrspundgdvdslem  34070  fldextrspundgdvds  34071  constrextdg2lem  34138  esumsplit  34443  esumpad2  34446  aean  34634  sxbrsigalem2  34676  bnj931  35159  tz9.1regs  35547  subfacp1lem2b  35673  subfacp1lem3  35674  subfacp1lem5  35676  kur14lem7  35704  kur14lem9  35706  cvmliftlem10  35786  satfsschain  35856  fmlasssuc  35881  refssfne  36869  filnetlem3  36891  bj-unrab  37562  bj-snglsstag  37617  bj-2upln0  37659  bj-ccssccbar  37861  rdgssun  38024  finixpnum  38256  matunitlindflem1  38267  mbfresfi  38317  prdsbnd  38444  heibor1lem  38460  rrnequiv  38486  paddunssN  40582  sspadd1  40589  sspadd2  40590  pclfinN  40674  dochdmj1  42164  dvhdimlem  42218  elrfi  43425  mzpcompact2lem  43482  eldioph2  43493  eldioph4b  43538  ttac  43763  pwssplit4  43816  pwslnmlem2  43820  isnumbasgrplem2  43831  algbase  43901  algaddg  43902  algmulr  43903  fiuneneq  43919  idomsubgmo  43920  onexlimgt  43970  omabs2  44059  tfsconcatrnss12  44076  rclexi  44341  rtrclex  44343  trclubgNEW  44344  trclexi  44346  rtrclexi  44347  cnvrcl0  44351  cnvtrcl0  44352  dfrtrcl5  44355  trrelsuperrel2dg  44397  dfrcl2  44400  relexp0a  44442  relexpaddss  44444  trclimalb2  44452  frege83d  44474  frege131d  44490  dssmapnvod  44746  clsk3nimkb  44766  isotone1  44774  grumnudlem  44995  dmwf  45674  infxrpnf  46160  mccllem  46313  cncfiooicclem1  46607  dvmptfprod  46659  dvnprodlem1  46660  iblsplit  46680  fourierdlem54  46874  fourierdlem102  46922  fourierdlem103  46923  fourierdlem104  46924  fourierdlem114  46934  sge0resplit  47120  sge0split  47123  sge0splitmpt  47125  sge0xaddlem1  47147  isomenndlem  47244  hoiprodp1  47302  hoidmvlelem1  47309  hoidmvlelem2  47310  hoidmvlelem3  47311  hoidmvlelem4  47312  dfnbgrss2  48624  gsumsplit2f  48945  setrec1lem4  50468  elpglem2  50490