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

Syntax hints:   ∨ wo 848   ∈ wcel 2114   ∪ cun 3900   ⊆ wss 3902

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 3443  df-un 3907  df-ss 3919

This theorem is referenced by:  ssun2  4132  ssun3  4133  elun1  4135  difsssymdif  4216  inabs  4219  reuun1  4281  un00  4398  pwunss  4573  pwundif  4579  snsspr1  4771  snsstp1  4773  snsstp2  4774  uniintsn  4941  sofld  6146  sssucid  6400  fvrn0  6863  f1ounsn  7220  ovima0  7539  unexb  7694  unexbOLD  7695  dmexg  7845  resf1extb  7878  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  9591  cantnfp1lem3  9593  tc2  9653  unwf  9726  rankunb  9766  r0weon  9926  infxpenlem  9927  dfac2b  10045  djudoml  10099  cdainflem  10102  infunabs  10120  infdju  10121  infdif  10122  ackbij1lem15  10147  cfsmolem  10184  isfin4p1  10229  fin23lem11  10231  fin1a2lem10  10323  fin1a2lem13  10326  axdc3lem4  10367  axcclem  10371  zornn0g  10419  ttukeylem1  10423  ttukeylem5  10427  ttukeylem7  10429  fingch  10538  fpwwe2lem12  10557  gchac  10596  wunfi  10636  wundm  10643  wunex2  10653  inar1  10690  ressxr  11180  nnssnn0  12408  un0addcl  12438  un0mulcl  12439  nn0ssxnn0  12481  hashbclem  14379  hashf1lem1  14382  hashf1lem2  14383  ccatrn  14517  trclublem  14922  relexpdmg  14969  relexpaddg  14980  fsumsplit  15668  fsum2d  15698  fsumabs  15728  fsumrlim  15738  fsumo1  15739  incexclem  15763  fprodsplit  15893  fprod2d  15908  lcmfunsnlem1  16568  coprmprod  16592  vdwapid1  16907  vdwlem6  16918  ramcl2  16948  isstruct2  17080  srngbase  17234  srngplusg  17235  srngmulr  17236  lmodbase  17250  lmodplusg  17251  lmodsca  17252  ipsbase  17261  ipsaddg  17262  ipsmulr  17263  phlbase  17271  phlplusg  17272  phlsca  17273  odrngbas  17328  odrngplusg  17329  odrngmulr  17330  prdssca  17380  prdsbas  17381  prdsplusg  17382  prdsmulr  17383  prdsvsca  17384  prdsip  17385  prdsle  17386  prdsds  17388  prdstset  17390  imasbas  17437  imasplusg  17442  imasmulr  17443  imassca  17444  imasvsca  17445  imasip  17446  mreexexlem2d  17572  drsdirfi  18232  ipobas  18458  ipotset  18460  acsfiindd  18480  psdmrn  18500  dirdm  18527  grpinvfval  18912  mulgfval  19003  gsumzsplit  19860  gsumsplit2  19862  gsumzunsnd  19889  gsum2dlem2  19904  dprdfadd  19955  dmdprdsplit2lem  19980  dmdprdsplit2  19981  dmdprdsplit  19982  dprdsplit  19983  ablfac1eulem  20007  gsumle  20078  lspun  20942  lspsolv  21102  lsppratlem3  21108  islbs3  21114  lbsextlem2  21118  lbsextlem4  21120  cnfldbas  21317  mpocnfldadd  21318  mpocnfldmul  21320  cnfldcj  21322  cnfldtset  21323  cnfldle  21324  cnfldds  21325  cnfldbasOLD  21332  cnfldaddOLD  21333  cnfldmulOLD  21334  cnfldcjOLD  21335  cnfldtsetOLD  21336  cnfldleOLD  21337  cnflddsOLD  21338  psrbas  21893  psrplusg  21896  psrmulr  21902  mplsubglem  21958  mplcoe1  21996  mplcoe5  21999  mdetunilem9  22568  basdif0  22901  ordtbas2  23139  ordtbas  23140  ordtopn1  23142  leordtval2  23160  iocpnfordt  23163  icomnfordt  23164  uncmp  23351  fiuncmp  23352  bwth  23358  locfincmp  23474  comppfsc  23480  1stckgenlem  23501  1stckgen  23502  ptbasin  23525  ptbasfi  23529  dfac14lem  23565  dfac14  23566  ptuncnv  23755  ptunhmeo  23756  ptcmpfi  23761  fbun  23788  trfil2  23835  ufprim  23857  ufileu  23867  filufint  23868  ufildr  23879  fmfnfm  23906  hausflim  23929  fclsfnflim  23975  alexsubALTlem4  23998  tmdgsum  24043  tsmsgsum  24087  tsmsres  24092  tsmssplit  24100  tsmsxplem1  24101  ustssco  24163  ustuqtop1  24189  prdsxmetlem  24316  prdsbl  24439  icccmplem2  24772  fsumcn  24821  cnmpopc  24882  rrxmetlem  25367  rrxmet  25368  rrxdstprj1  25369  ovolctb2  25453  ovolunnul  25461  ovolfiniun  25462  nulmbl2  25497  finiunmbl  25505  volfiniun  25508  icombl  25525  ioombl  25526  uniiccdif  25539  mbfres2  25606  itg2splitlem  25709  itg2split  25710  itgfsum  25788  itgsplit  25797  itgsplitioo  25799  dvreslem  25870  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvmptfsum  25939  lhop  25981  dvcnvrelem2  25983  mdegcl  26034  elplyr  26166  plyrem  26273  xrlimcnp  26938  fsumharmonic  26982  chtdif  27128  lgsdir2lem3  27298  lgsquadlem2  27352  dchrisum0lem1b  27486  pntrlog2bndlem6  27554  pntlemf  27576  nosupinfsep  27704  noetalem1  27713  scutun12  27788  cofcutrtime  27909  addsuniflem  27983  addsbday  28000  negsval  28007  mulsproplem12  28109  mulsproplem13  28110  mulsproplem14  28111  mulsuniflem  28131  mulsass  28148  precsexlem6  28193  precsexlem7  28194  precsexlem10  28197  precsexlem11  28198  ex-ss  30485  shsleji  31428  shsval2i  31445  ssjo  31505  sshhococi  31604  padct  32778  symgcom  33146  cycpmco2lem5  33193  cycpmco2lem6  33194  cycpmco2lem7  33195  cycpmco2  33196  gsumvsca1  33289  gsumvsca2  33290  elrgspnsubrunlem1  33310  rlocbas  33330  rlocaddval  33331  rlocmulval  33332  elrspunsn  33491  mxidlprm  33532  idlsrgbas  33566  idlsrgplusg  33567  idlsrgmulr  33569  fldextrspundgdvdslem  33818  fldextrspundgdvds  33819  constrextdg2lem  33886  esumsplit  34191  esumpad2  34194  aean  34382  sxbrsigalem2  34424  bnj931  34907  tz9.1regs  35271  subfacp1lem2b  35356  subfacp1lem3  35357  subfacp1lem5  35359  kur14lem7  35387  kur14lem9  35389  cvmliftlem10  35469  satfsschain  35539  fmlasssuc  35564  refssfne  36533  filnetlem3  36555  bj-unrab  37102  bj-snglsstag  37157  bj-2upln0  37199  bj-ccssccbar  37393  rdgssun  37554  finixpnum  37777  matunitlindflem1  37788  mbfresfi  37838  prdsbnd  37965  heibor1lem  37981  rrnequiv  38007  paddunssN  40105  sspadd1  40112  sspadd2  40113  pclfinN  40197  dochdmj1  41687  dvhdimlem  41741  elrfi  42972  mzpcompact2lem  43029  eldioph2  43040  eldioph4b  43089  ttac  43314  pwssplit4  43367  pwslnmlem2  43371  isnumbasgrplem2  43382  algbase  43452  algaddg  43453  algmulr  43454  fiuneneq  43470  idomsubgmo  43471  onexlimgt  43521  omabs2  43610  tfsconcatrnss12  43627  rclexi  43892  rtrclex  43894  trclubgNEW  43895  trclexi  43897  rtrclexi  43898  cnvrcl0  43902  cnvtrcl0  43903  dfrtrcl5  43906  trrelsuperrel2dg  43948  dfrcl2  43951  relexp0a  43993  relexpaddss  43995  trclimalb2  44003  frege83d  44025  frege131d  44041  dssmapnvod  44297  clsk3nimkb  44317  isotone1  44325  grumnudlem  44562  dmwf  45242  infxrpnf  45726  mccllem  45879  cncfiooicclem1  46173  dvmptfprod  46225  dvnprodlem1  46226  iblsplit  46246  fourierdlem54  46440  fourierdlem102  46488  fourierdlem103  46489  fourierdlem104  46490  fourierdlem114  46500  sge0resplit  46686  sge0split  46689  sge0splitmpt  46691  sge0xaddlem1  46713  isomenndlem  46810  hoiprodp1  46868  hoidmvlelem1  46875  hoidmvlelem2  46876  hoidmvlelem3  46877  hoidmvlelem4  46878  dfnbgrss2  48141  gsumsplit2f  48462  setrec1lem4  49971  elpglem2  49993