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

This proof depends on syntax axioms:   ∨ wo 861   ∈ wcel 2146   ∪ cun 3904   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923

This theorem is used by:  ssun2  4132  ssun3  4133  elun1  4135  difsssymdif  4216  inabs  4219  reuun1  4281  un00  4364  pwunss  4582  pwundif  4589  snsspr1  4782  snsstp1  4784  snsstp2  4785  uniintsn  4952  sofld  6187  relresfld  6280  sssucid  6447  fvrn0  6913  f1ounsn  7279  ovima0  7599  unexb  7754  dmexg  7904  resf1extb  7937  xpord2indlem  8149  xpord3inddlem  8156  suppun  8186  dftpos2  8245  tpostpos2  8249  frrlem12  8300  frrlem13  8301  tfrlem11  8381  oaabs2  8641  ralxpmap  8900  domss2  9131  mapunen  9141  ac6sfi  9251  frfi  9252  unfir  9275  domunfican  9288  iunfi  9307  elfiun  9397  dffi3  9398  unwdomg  9553  unxpwdom2  9557  unxpwdom  9558  cantnfp1lem1  9654  cantnfp1lem3  9656  tc2  9716  unwf  9789  rankunb  9829  r0weon  10012  infxpenlem  10013  dfac2b  10130  djudoml  10184  cdainflem  10187  infunabs  10205  infdju  10206  infdif  10207  ackbij1lem15  10232  cfsmolem  10269  isfin4p1  10314  fin23lem11  10316  fin1a2lem10  10408  fin1a2lem13  10411  axdc3lem4  10452  axcclem  10456  zornn0g  10504  ttukeylem1  10508  ttukeylem5  10512  ttukeylem7  10514  fingch  10623  fpwwe2lem12  10642  gchac  10681  wunfi  10721  wundm  10728  wunex2  10738  inar1  10775  ressxr  11268  nnssnn0  12522  un0addcl  12552  un0mulcl  12553  nn0ssxnn0  12595  hashbclem  14507  hashf1lem1  14510  hashf1lem2  14511  ccatrn  14645  trclublem  15056  relexpdmg  15103  relexpaddg  15114  fsumsplit  15815  fsum2d  15845  fsumabs  15876  fsumrlim  15886  fsumo1  15887  incexclem  15913  fprodsplit  16043  fprod2d  16058  lcmfunsnlem1  16717  coprmprod  16741  vdwapid1  17057  vdwlem6  17068  ramcl2  17098  isstruct2  17231  srngbase  17385  srngplusg  17386  srngmulr  17387  lmodbase  17401  lmodplusg  17402  lmodsca  17403  ipsbase  17412  ipsaddg  17413  ipsmulr  17414  phlbase  17422  phlplusg  17423  phlsca  17424  odrngbas  17479  odrngplusg  17480  odrngmulr  17481  prdssca  17531  prdsbas  17532  prdsplusg  17533  prdsmulr  17534  prdsvsca  17535  prdsip  17536  prdsle  17537  prdsds  17539  prdstset  17541  imasbas  17588  imasplusg  17593  imasmulr  17594  imassca  17595  imasvsca  17596  imasip  17597  mreexexlem2d  17723  drsdirfi  18383  ipobas  18609  ipotset  18611  acsfiindd  18631  psdmrn  18651  dirdm  18678  grpinvfval  19089  mulgfval  19179  gsumzsplit  20041  gsumsplit2  20043  gsumzunsnd  20070  gsum2dlem2  20085  dprdfadd  20136  dmdprdsplit2lem  20161  dmdprdsplit2  20162  dmdprdsplit  20163  dprdsplit  20164  ablfac1eulem  20188  gsumle  20259  lspun  21158  lspsolv  21317  lsppratlem3  21323  islbs3  21329  lbsextlem2  21333  lbsextlem4  21335  cnfldbas  21576  mpocnfldadd  21577  mpocnfldmul  21579  cnfldcj  21581  cnfldtset  21582  cnfldle  21583  cnfldds  21584  psrbas  22134  psrplusg  22137  psrmulr  22142  mplsubglem  22198  mplcoe1  22238  mplcoe5  22241  mdetunilem9  22827  basdif0  23160  ordtbas2  23398  ordtbas  23399  ordtopn1  23401  leordtval2  23419  iocpnfordt  23422  icomnfordt  23423  uncmp  23610  fiuncmp  23611  bwth  23617  locfincmp  23734  comppfsc  23740  1stckgenlem  23761  1stckgen  23762  ptbasin  23785  ptbasfi  23789  dfac14lem  23825  dfac14  23826  ptuncnv  24015  ptunhmeo  24016  ptcmpfi  24021  fbun  24048  trfil2  24095  ufprim  24117  ufileu  24127  filufint  24128  ufildr  24139  fmfnfm  24166  hausflim  24189  fclsfnflim  24235  alexsubALTlem4  24258  tmdgsum  24303  tsmsgsum  24347  tsmsres  24352  tsmssplit  24360  tsmsxplem1  24361  ustssco  24423  ustuqtop1  24449  prdsxmetlem  24576  prdsbl  24699  icccmplem2  25032  fsumcn  25080  cnmpopc  25138  rrxmetlem  25617  rrxmet  25618  rrxdstprj1  25619  ovolctb2  25702  ovolunnul  25710  ovolfiniun  25711  nulmbl2  25746  finiunmbl  25754  volfiniun  25757  icombl  25774  ioombl  25775  uniiccdif  25788  mbfres2  25855  itg2splitlem  25958  itg2split  25959  itgfsum  26037  itgsplit  26046  itgsplitioo  26048  dvreslem  26119  dvaddbr  26148  dvmulbr  26149  dvmptfsum  26185  lhop  26226  dvcnvrelem2  26228  mdegcl  26277  elplyr  26409  plyrem  26517  xrlimcnp  27184  fsumharmonic  27227  chtdif  27373  lgsdir2lem3  27542  lgsquadlem2  27596  dchrisum0lem1b  27730  pntrlog2bndlem6  27798  pntlemf  27820  nosupinfsep  27947  noetalem1  27956  cutsun12  28034  cofcutrtime  28171  addsuniflem  28245  addbday  28262  negsval  28269  mulsproplem12  28371  mulsproplem13  28372  mulsproplem14  28373  mulsuniflem  28393  mulsass  28410  precsexlem6  28456  precsexlem7  28457  precsexlem10  28460  precsexlem11  28461  ex-ss  30849  shsleji  31793  shsval2i  31810  ssjo  31870  sshhococi  31969  padct  33133  symgcom  33467  cycpmco2lem5  33514  cycpmco2lem6  33515  cycpmco2lem7  33516  cycpmco2  33517  gsumvsca1  33610  gsumvsca2  33611  elrgspnsubrunlem1  33631  rlocbas  33652  rlocaddval  33653  rlocmulval  33654  elrspunsn  33801  mxidlprm  33817  idlsrgbas  33858  idlsrgplusg  33859  idlsrgmulr  33861  fldextrspundgdvdslem  34134  fldextrspundgdvds  34135  constrextdg2lem  34202  esumsplit  34507  esumpad2  34510  aean  34699  sxbrsigalem2  34741  bnj931  35224  tz9.1regs  35604  subfacp1lem2b  35710  subfacp1lem3  35711  subfacp1lem5  35713  kur14lem7  35741  kur14lem9  35743  cvmliftlem10  35823  satfsschain  35893  fmlasssuc  35918  refssfne  36926  filnetlem3  36948  bj-unrab  37619  bj-snglsstag  37674  bj-2upln0  37716  bj-ccssccbar  37918  rdgssun  38081  finixpnum  38313  matunitlindflem1  38324  mbfresfi  38374  prdsbnd  38502  heibor1lem  38518  rrnequiv  38544  paddunssN  40640  sspadd1  40647  sspadd2  40648  pclfinN  40732  dochdmj1  42222  dvhdimlem  42276  elrfi  43483  mzpcompact2lem  43540  eldioph2  43551  eldioph4b  43596  ttac  43821  pwssplit4  43874  pwslnmlem2  43878  isnumbasgrplem2  43889  algbase  43959  algaddg  43960  algmulr  43961  fiuneneq  43977  idomsubgmo  43978  onexlimgt  44028  omabs2  44117  tfsconcatrnss12  44134  rclexi  44399  rtrclex  44401  trclubgNEW  44402  trclexi  44404  rtrclexi  44405  cnvrcl0  44409  cnvtrcl0  44410  dfrtrcl5  44413  trrelsuperrel2dg  44455  dfrcl2  44458  relexp0a  44500  relexpaddss  44502  trclimalb2  44510  frege83d  44532  frege131d  44548  dssmapnvod  44804  clsk3nimkb  44824  isotone1  44832  grumnudlem  45053  dmwf  45732  infxrpnf  46218  mccllem  46371  cncfiooicclem1  46665  dvmptfprod  46717  dvnprodlem1  46718  iblsplit  46738  fourierdlem54  46932  fourierdlem102  46980  fourierdlem103  46981  fourierdlem104  46982  fourierdlem114  46992  sge0resplit  47178  sge0split  47181  sge0splitmpt  47183  sge0xaddlem1  47205  isomenndlem  47302  hoiprodp1  47360  hoidmvlelem1  47367  hoidmvlelem2  47368  hoidmvlelem3  47369  hoidmvlelem4  47370  dfnbgrss2  48682  gsumsplit2f  49002  setrec1lem4  50525  elpglem2  50547