Theorem ssun1 4171

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

Syntax hints:   ∨ wo 846   ∈ wcel 2107   ∪ cun 3945   ⊆ wss 3947

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3952  df-in 3954  df-ss 3964

This theorem is referenced by:  ssun2  4172  ssun3  4173  elun1  4175  difsssymdif  4251  inabs  4254  reuun1  4316  un00  4441  pwunss  4619  pwundif  4625  snsspr1  4816  snsstp1  4818  snsstp2  4819  uniintsn  4990  sofld  6183  sssucid  6441  fvrn0  6918  ovima0  7581  unexb  7730  dmexg  7889  xpord2indlem  8128  xpord3inddlem  8135  suppun  8164  dftpos2  8223  tpostpos2  8227  frrlem12  8277  frrlem13  8278  wfrlem14OLD  8317  wfrlem15OLD  8318  tfrlem11  8383  oaabs2  8644  ralxpmap  8886  domss2  9132  mapunen  9142  ac6sfi  9283  frfi  9284  unfir  9310  domunfican  9316  iunfi  9336  elfiun  9421  dffi3  9422  unwdomg  9575  unxpwdom2  9579  unxpwdom  9580  cantnfp1lem1  9669  cantnfp1lem3  9671  tc2  9733  unwf  9801  rankunb  9841  r0weon  10003  infxpenlem  10004  dfac2b  10121  djudoml  10175  cdainflem  10178  infunabs  10198  infdju  10199  infdif  10200  ackbij1lem15  10225  cfsmolem  10261  isfin4p1  10306  fin23lem11  10308  fin1a2lem10  10400  fin1a2lem13  10403  axdc3lem4  10444  axcclem  10448  zornn0g  10496  ttukeylem1  10500  ttukeylem5  10504  ttukeylem7  10506  fingch  10614  fpwwe2lem12  10633  gchac  10672  wunfi  10712  wundm  10719  wunex2  10729  inar1  10766  ressxr  11254  nnssnn0  12471  un0addcl  12501  un0mulcl  12502  nn0ssxnn0  12543  hashbclem  14407  hashf1lem1  14411  hashf1lem1OLD  14412  hashf1lem2  14413  ccatrn  14535  trclublem  14938  relexpdmg  14985  relexpaddg  14996  fsumsplit  15683  fsum2d  15713  fsumabs  15743  fsumrlim  15753  fsumo1  15754  incexclem  15778  fprodsplit  15906  fprod2d  15921  lcmfunsnlem1  16570  coprmprod  16594  vdwapid1  16904  vdwlem6  16915  ramcl2  16945  isstruct2  17078  srngbase  17251  srngplusg  17252  srngmulr  17253  lmodbase  17267  lmodplusg  17268  lmodsca  17269  ipsbase  17278  ipsaddg  17279  ipsmulr  17280  phlbase  17288  phlplusg  17289  phlsca  17290  odrngbas  17345  odrngplusg  17346  odrngmulr  17347  prdssca  17398  prdsbas  17399  prdsplusg  17400  prdsmulr  17401  prdsvsca  17402  prdsip  17403  prdsle  17404  prdsds  17406  prdstset  17408  imasbas  17454  imasplusg  17459  imasmulr  17460  imassca  17461  imasvsca  17462  imasip  17463  mreexexlem2d  17585  drsdirfi  18254  ipobas  18480  ipotset  18482  acsfiindd  18502  psdmrn  18522  dirdm  18549  grpinvfval  18859  mulgfval  18946  gsumzsplit  19787  gsumsplit2  19789  gsumzunsnd  19816  gsum2dlem2  19831  dprdfadd  19882  dmdprdsplit2lem  19907  dmdprdsplit2  19908  dmdprdsplit  19909  dprdsplit  19910  ablfac1eulem  19934  lspun  20586  lspsolv  20744  lsppratlem3  20750  islbs3  20756  lbsextlem2  20760  lbsextlem4  20762  cnfldbas  20933  cnfldadd  20934  cnfldmul  20935  cnfldcj  20936  cnfldtset  20937  cnfldle  20938  cnfldds  20939  psrbagaddclOLD  21464  psrbas  21479  psrplusg  21482  psrmulr  21485  mplsubglem  21540  mplcoe1  21574  mplcoe5  21577  mdetunilem9  22104  basdif0  22438  ordtbas2  22677  ordtbas  22678  ordtopn1  22680  leordtval2  22698  iocpnfordt  22701  icomnfordt  22702  uncmp  22889  fiuncmp  22890  bwth  22896  locfincmp  23012  comppfsc  23018  1stckgenlem  23039  1stckgen  23040  ptbasin  23063  ptbasfi  23067  dfac14lem  23103  dfac14  23104  ptuncnv  23293  ptunhmeo  23294  ptcmpfi  23299  fbun  23326  trfil2  23373  ufprim  23395  ufileu  23405  filufint  23406  ufildr  23417  fmfnfm  23444  hausflim  23467  fclsfnflim  23513  alexsubALTlem4  23536  tmdgsum  23581  tsmsgsum  23625  tsmsres  23630  tsmssplit  23638  tsmsxplem1  23639  ustssco  23701  ustuqtop1  23728  prdsxmetlem  23856  prdsbl  23982  icccmplem2  24321  fsumcn  24368  cnmpopc  24426  rrxmetlem  24906  rrxmet  24907  rrxdstprj1  24908  ovolctb2  24991  ovolunnul  24999  ovolfiniun  25000  nulmbl2  25035  finiunmbl  25043  volfiniun  25046  icombl  25063  ioombl  25064  uniiccdif  25077  mbfres2  25144  itg2splitlem  25248  itg2split  25249  itgfsum  25326  itgsplit  25335  itgsplitioo  25337  dvreslem  25408  dvaddbr  25437  dvmulbr  25438  dvmptfsum  25474  lhop  25515  dvcnvrelem2  25517  mdegcl  25569  elplyr  25697  plyrem  25800  xrlimcnp  26453  fsumharmonic  26496  chtdif  26642  lgsdir2lem3  26810  lgsquadlem2  26864  dchrisum0lem1b  26998  pntrlog2bndlem6  27066  pntlemf  27088  nosupinfsep  27215  noetalem1  27224  scutun12  27291  cofcutrtime  27394  addsuniflem  27464  negsval  27480  mulsproplem12  27563  mulsproplem13  27564  mulsproplem14  27565  mulsuniflem  27584  mulsass  27601  precsexlem6  27638  precsexlem7  27639  precsexlem10  27642  precsexlem11  27643  ex-ss  29660  shsleji  30601  shsval2i  30618  ssjo  30678  sshhococi  30777  padct  31922  gsumle  32220  symgcom  32222  cycpmco2lem5  32267  cycpmco2lem6  32268  cycpmco2lem7  32269  cycpmco2  32270  gsumvsca1  32349  gsumvsca2  32350  elrspunsn  32505  mxidlprm  32544  idlsrgbas  32570  idlsrgplusg  32571  idlsrgmulr  32573  esumsplit  32989  esumpad2  32992  aean  33180  sxbrsigalem2  33223  bnj931  33719  subfacp1lem2b  34110  subfacp1lem3  34111  subfacp1lem5  34113  kur14lem7  34141  kur14lem9  34143  cvmliftlem10  34223  satfsschain  34293  fmlasssuc  34318  gg-dvmulbr  35113  refssfne  35181  filnetlem3  35203  bj-unrab  35744  bj-snglsstag  35800  bj-2upln0  35842  bj-ccssccbar  36036  rdgssun  36197  finixpnum  36411  matunitlindflem1  36422  mbfresfi  36472  prdsbnd  36599  heibor1lem  36615  rrnequiv  36641  paddunssN  38617  sspadd1  38624  sspadd2  38625  pclfinN  38709  dochdmj1  40199  dvhdimlem  40253  elrfi  41365  mzpcompact2lem  41422  eldioph2  41433  eldioph4b  41482  ttac  41708  pwssplit4  41764  pwslnmlem2  41768  isnumbasgrplem2  41779  algbase  41853  algaddg  41854  algmulr  41855  fiuneneq  41872  idomsubgmo  41873  onexlimgt  41925  omabs2  42015  tfsconcatrnss12  42032  rclexi  42299  rtrclex  42301  trclubgNEW  42302  trclexi  42304  rtrclexi  42305  cnvrcl0  42309  cnvtrcl0  42310  dfrtrcl5  42313  trrelsuperrel2dg  42355  dfrcl2  42358  relexp0a  42400  relexpaddss  42402  trclimalb2  42410  frege83d  42432  frege131d  42448  dssmapnvod  42704  clsk3nimkb  42724  isotone1  42732  grumnudlem  42977  infxrpnf  44091  mccllem  44248  cncfiooicclem1  44544  dvmptfprod  44596  dvnprodlem1  44597  iblsplit  44617  fourierdlem54  44811  fourierdlem102  44859  fourierdlem103  44860  fourierdlem104  44861  fourierdlem114  44871  sge0resplit  45057  sge0split  45060  sge0splitmpt  45062  sge0xaddlem1  45084  isomenndlem  45181  hoiprodp1  45239  hoidmvlelem1  45246  hoidmvlelem2  45247  hoidmvlelem3  45248  hoidmvlelem4  45249  gsumsplit2f  46525  setrec1lem4  47637  elpglem2  47659