Theorem ssun1 4119

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

Syntax hints:   ∨ wo 848   ∈ wcel 2114   ∪ cun 3888   ⊆ wss 3890

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 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  ssun2  4120  ssun3  4121  elun1  4123  difsssymdif  4204  inabs  4207  reuun1  4269  un00  4386  pwunss  4560  pwundif  4566  snsspr1  4758  snsstp1  4760  snsstp2  4761  uniintsn  4928  sofld  6146  sssucid  6400  fvrn0  6863  f1ounsn  7221  ovima0  7540  unexb  7695  unexbOLD  7696  dmexg  7846  resf1extb  7879  xpord2indlem  8091  xpord3inddlem  8098  suppun  8128  dftpos2  8187  tpostpos2  8191  frrlem12  8241  frrlem13  8242  tfrlem11  8321  oaabs2  8579  ralxpmap  8838  domss2  9068  mapunen  9078  ac6sfi  9188  frfi  9189  unfir  9212  domunfican  9226  iunfi  9247  elfiun  9337  dffi3  9338  unwdomg  9493  unxpwdom2  9497  unxpwdom  9498  cantnfp1lem1  9593  cantnfp1lem3  9595  tc2  9655  unwf  9728  rankunb  9768  r0weon  9928  infxpenlem  9929  dfac2b  10047  djudoml  10101  cdainflem  10104  infunabs  10122  infdju  10123  infdif  10124  ackbij1lem15  10149  cfsmolem  10186  isfin4p1  10231  fin23lem11  10233  fin1a2lem10  10325  fin1a2lem13  10328  axdc3lem4  10369  axcclem  10373  zornn0g  10421  ttukeylem1  10425  ttukeylem5  10429  ttukeylem7  10431  fingch  10540  fpwwe2lem12  10559  gchac  10598  wunfi  10638  wundm  10645  wunex2  10655  inar1  10692  ressxr  11183  nnssnn0  12434  un0addcl  12464  un0mulcl  12465  nn0ssxnn0  12507  hashbclem  14408  hashf1lem1  14411  hashf1lem2  14412  ccatrn  14546  trclublem  14951  relexpdmg  14998  relexpaddg  15009  fsumsplit  15697  fsum2d  15727  fsumabs  15758  fsumrlim  15768  fsumo1  15769  incexclem  15795  fprodsplit  15925  fprod2d  15940  lcmfunsnlem1  16600  coprmprod  16624  vdwapid1  16940  vdwlem6  16951  ramcl2  16981  isstruct2  17113  srngbase  17267  srngplusg  17268  srngmulr  17269  lmodbase  17283  lmodplusg  17284  lmodsca  17285  ipsbase  17294  ipsaddg  17295  ipsmulr  17296  phlbase  17304  phlplusg  17305  phlsca  17306  odrngbas  17361  odrngplusg  17362  odrngmulr  17363  prdssca  17413  prdsbas  17414  prdsplusg  17415  prdsmulr  17416  prdsvsca  17417  prdsip  17418  prdsle  17419  prdsds  17421  prdstset  17423  imasbas  17470  imasplusg  17475  imasmulr  17476  imassca  17477  imasvsca  17478  imasip  17479  mreexexlem2d  17605  drsdirfi  18265  ipobas  18491  ipotset  18493  acsfiindd  18513  psdmrn  18533  dirdm  18560  grpinvfval  18948  mulgfval  19039  gsumzsplit  19896  gsumsplit2  19898  gsumzunsnd  19925  gsum2dlem2  19940  dprdfadd  19991  dmdprdsplit2lem  20016  dmdprdsplit2  20017  dmdprdsplit  20018  dprdsplit  20019  ablfac1eulem  20043  gsumle  20114  lspun  20976  lspsolv  21136  lsppratlem3  21142  islbs3  21148  lbsextlem2  21152  lbsextlem4  21154  cnfldbas  21351  mpocnfldadd  21352  mpocnfldmul  21354  cnfldcj  21356  cnfldtset  21357  cnfldle  21358  cnfldds  21359  cnfldbasOLD  21366  cnfldaddOLD  21367  cnfldmulOLD  21368  cnfldcjOLD  21369  cnfldtsetOLD  21370  cnfldleOLD  21371  cnflddsOLD  21372  psrbas  21926  psrplusg  21929  psrmulr  21934  mplsubglem  21990  mplcoe1  22028  mplcoe5  22031  mdetunilem9  22598  basdif0  22931  ordtbas2  23169  ordtbas  23170  ordtopn1  23172  leordtval2  23190  iocpnfordt  23193  icomnfordt  23194  uncmp  23381  fiuncmp  23382  bwth  23388  locfincmp  23504  comppfsc  23510  1stckgenlem  23531  1stckgen  23532  ptbasin  23555  ptbasfi  23559  dfac14lem  23595  dfac14  23596  ptuncnv  23785  ptunhmeo  23786  ptcmpfi  23791  fbun  23818  trfil2  23865  ufprim  23887  ufileu  23897  filufint  23898  ufildr  23909  fmfnfm  23936  hausflim  23959  fclsfnflim  24005  alexsubALTlem4  24028  tmdgsum  24073  tsmsgsum  24117  tsmsres  24122  tsmssplit  24130  tsmsxplem1  24131  ustssco  24193  ustuqtop1  24219  prdsxmetlem  24346  prdsbl  24469  icccmplem2  24802  fsumcn  24850  cnmpopc  24908  rrxmetlem  25387  rrxmet  25388  rrxdstprj1  25389  ovolctb2  25472  ovolunnul  25480  ovolfiniun  25481  nulmbl2  25516  finiunmbl  25524  volfiniun  25527  icombl  25544  ioombl  25545  uniiccdif  25558  mbfres2  25625  itg2splitlem  25728  itg2split  25729  itgfsum  25807  itgsplit  25816  itgsplitioo  25818  dvreslem  25889  dvaddbr  25918  dvmulbr  25919  dvmptfsum  25955  lhop  25996  dvcnvrelem2  25998  mdegcl  26047  elplyr  26179  plyrem  26285  xrlimcnp  26948  fsumharmonic  26992  chtdif  27138  lgsdir2lem3  27307  lgsquadlem2  27361  dchrisum0lem1b  27495  pntrlog2bndlem6  27563  pntlemf  27585  nosupinfsep  27713  noetalem1  27722  cutsun12  27799  cofcutrtime  27936  addsuniflem  28010  addbday  28027  negsval  28034  mulsproplem12  28136  mulsproplem13  28137  mulsproplem14  28138  mulsuniflem  28158  mulsass  28175  precsexlem6  28221  precsexlem7  28222  precsexlem10  28225  precsexlem11  28226  ex-ss  30515  shsleji  31459  shsval2i  31476  ssjo  31536  sshhococi  31635  padct  32809  symgcom  33162  cycpmco2lem5  33209  cycpmco2lem6  33210  cycpmco2lem7  33211  cycpmco2  33212  gsumvsca1  33305  gsumvsca2  33306  elrgspnsubrunlem1  33326  rlocbas  33346  rlocaddval  33347  rlocmulval  33348  elrspunsn  33507  mxidlprm  33548  idlsrgbas  33582  idlsrgplusg  33583  idlsrgmulr  33585  fldextrspundgdvdslem  33843  fldextrspundgdvds  33844  constrextdg2lem  33911  esumsplit  34216  esumpad2  34219  aean  34407  sxbrsigalem2  34449  bnj931  34932  tz9.1regs  35297  subfacp1lem2b  35382  subfacp1lem3  35383  subfacp1lem5  35385  kur14lem7  35413  kur14lem9  35415  cvmliftlem10  35495  satfsschain  35565  fmlasssuc  35590  refssfne  36559  filnetlem3  36581  bj-unrab  37252  bj-snglsstag  37307  bj-2upln0  37349  bj-ccssccbar  37550  rdgssun  37711  finixpnum  37943  matunitlindflem1  37954  mbfresfi  38004  prdsbnd  38131  heibor1lem  38147  rrnequiv  38173  paddunssN  40271  sspadd1  40278  sspadd2  40279  pclfinN  40363  dochdmj1  41853  dvhdimlem  41907  elrfi  43143  mzpcompact2lem  43200  eldioph2  43211  eldioph4b  43260  ttac  43485  pwssplit4  43538  pwslnmlem2  43542  isnumbasgrplem2  43553  algbase  43623  algaddg  43624  algmulr  43625  fiuneneq  43641  idomsubgmo  43642  onexlimgt  43692  omabs2  43781  tfsconcatrnss12  43798  rclexi  44063  rtrclex  44065  trclubgNEW  44066  trclexi  44068  rtrclexi  44069  cnvrcl0  44073  cnvtrcl0  44074  dfrtrcl5  44077  trrelsuperrel2dg  44119  dfrcl2  44122  relexp0a  44164  relexpaddss  44166  trclimalb2  44174  frege83d  44196  frege131d  44212  dssmapnvod  44468  clsk3nimkb  44488  isotone1  44496  grumnudlem  44733  dmwf  45413  infxrpnf  45895  mccllem  46048  cncfiooicclem1  46342  dvmptfprod  46394  dvnprodlem1  46395  iblsplit  46415  fourierdlem54  46609  fourierdlem102  46657  fourierdlem103  46658  fourierdlem104  46659  fourierdlem114  46669  sge0resplit  46855  sge0split  46858  sge0splitmpt  46860  sge0xaddlem1  46882  isomenndlem  46979  hoiprodp1  47037  hoidmvlelem1  47044  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvlelem4  47047  dfnbgrss2  48350  gsumsplit2f  48671  setrec1lem4  50180  elpglem2  50202