Theorem ssun1 4175

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

This proof depends on syntax axioms:   ∨ wo 861   ∈ wcel 2144   ⊆ wss 3896   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150

This theorem is used by:  ssun2  4176  ssun3  4177  elun1  4179  difsssymdif  4207  inabs  4210  reuun1  4272  un00  4356  pwunss  4575  pwundif  4582  snsspr1  4769  snsstp1  4771  snsstp2  4772  uniintsn  4944  sofld  6181  relresfld  6281  sssucid  6448  fvrn0  6918  f1ounsn  7284  ovima0  7604  unexb  7767  dmexg  7917  resf1extb  7950  xpord2indlem  8171  xpord3inddlem  8178  suppun  8209  dftpos2  8268  tpostpos2  8272  frrlem12  8323  frrlem13  8324  tfrlem11  8404  oaabs2  8666  ralxpmap  8932  domss2  9163  mapunen  9173  ac6sfi  9283  frfi  9284  unfir  9308  domunfican  9321  iunfi  9340  elfiun  9429  dffi3  9430  unwdomg  9585  unxpwdom2  9589  unxpwdom  9590  cantnfp1lem1  9686  cantnfp1lem3  9688  tc2  9748  unwf  9825  rankunb  9871  setrec1lem4  9978  r0weon  10098  infxpenlem  10099  dfac2b  10216  djudoml  10270  cdainflem  10273  infunabs  10291  infdju  10292  infdif  10293  ackbij1lem15  10318  cfsmolem  10355  isfin4p1  10400  fin23lem11  10402  fin1a2lem10  10494  fin1a2lem13  10497  axdc3lem4  10538  axcclem  10542  zornn0g  10590  ttukeylem1  10594  ttukeylem5  10598  ttukeylem7  10600  fingch  10715  fpwwe2lem12  10734  gchac  10773  wunfi  10813  wundm  10820  wunex2  10830  inar1  10867  ressxr  11360  nnssnn0  12616  un0addcl  12646  un0mulcl  12647  nn0ssxnn0  12689  hashbclem  14604  hashf1lem1  14607  hashf1lem2  14608  ccatrn  14742  trclublem  15157  relexpdmg  15204  relexpaddg  15215  fsumsplit  15916  fsum2d  15946  fsumabs  15977  fsumrlim  15987  fsumo1  15988  incexclem  16014  fprodsplit  16142  fprod2d  16157  lcmfunsnlem1  16821  coprmprod  16845  vdwapid1  17162  vdwlem6  17173  ramcl2  17203  isstruct2  17336  srngbase  17490  srngplusg  17491  srngmulr  17492  lmodbase  17506  lmodplusg  17507  lmodsca  17508  ipsbase  17517  ipsaddg  17518  ipsmulr  17519  phlbase  17527  phlplusg  17528  phlsca  17529  odrngbas  17584  odrngplusg  17585  odrngmulr  17586  prdssca  17636  prdsbas  17637  prdsplusg  17638  prdsmulr  17639  prdsvsca  17640  prdsip  17641  prdsle  17642  prdsds  17644  prdstset  17646  imasbas  17693  imasplusg  17698  imasmulr  17699  imassca  17700  imasvsca  17701  imasip  17702  mreexexlem2d  17828  drsdirfi  18488  ipobas  18714  ipotset  18716  acsfiindd  18736  psdmrn  18756  dirdm  18783  grpinvfval  19198  mulgfval  19288  gsumzsplit  20150  gsumsplit2  20152  gsumzunsnd  20179  gsum2dlem2  20194  dprdfadd  20245  dmdprdsplit2lem  20270  dmdprdsplit2  20271  dmdprdsplit  20272  dprdsplit  20273  ablfac1eulem  20297  gsumle  20368  lspun  21271  lspsolv  21430  lsppratlem3  21436  islbs3  21442  lbsextlem2  21446  lbsextlem4  21448  cnfldbas  21691  mpocnfldadd  21692  mpocnfldmul  21694  cnfldcj  21696  cnfldtset  21697  cnfldle  21698  cnfldds  21699  psrbas  22251  psrplusg  22254  psrmulr  22259  mplsubglem  22315  mplcoe1  22355  mplcoe5  22358  mdetunilem9  22944  matunitlindflem1  23003  basdif0  23280  ordtbas2  23518  ordtbas  23519  ordtopn1  23521  leordtval2  23539  iocpnfordt  23542  icomnfordt  23543  uncmp  23730  fiuncmp  23731  bwth  23737  locfincmp  23854  comppfsc  23860  1stckgenlem  23881  1stckgen  23882  ptbasin  23905  ptbasfi  23909  dfac14lem  23945  dfac14  23946  ptuncnv  24135  ptunhmeo  24136  ptcmpfi  24141  fbun  24168  trfil2  24215  ufprim  24237  ufileu  24247  filufint  24248  ufildr  24259  fmfnfm  24286  hausflim  24309  fclsfnflim  24355  alexsubALTlem4  24378  tmdgsum  24423  tsmsgsum  24467  tsmsres  24472  tsmssplit  24480  tsmsxplem1  24481  ustssco  24543  ustuqtop1  24569  prdsxmetlem  24696  prdsbl  24819  icccmplem2  25152  fsumcn  25200  cnmpopc  25258  rrxmetlem  25737  rrxmet  25738  rrxdstprj1  25739  ovolctb2  25822  ovolunnul  25830  ovolfiniun  25831  nulmbl2  25866  finiunmbl  25874  volfiniun  25877  icombl  25894  ioombl  25895  uniiccdif  25908  mbfres2  25975  itg2splitlem  26078  itg2split  26079  itgfsum  26156  itgsplit  26165  itgsplitioo  26167  dvreslem  26238  dvaddbr  26267  dvmulbr  26268  dvmptfsum  26304  lhop  26345  dvcnvrelem2  26347  mdegcl  26396  elplyr  26528  plyrem  26635  xrlimcnp  27305  fsumharmonic  27348  chtdif  27494  lgsdir2lem3  27663  lgsquadlem2  27717  dchrisum0lem1b  27851  pntrlog2bndlem6  27919  pntlemf  27941  nosupinfsep  28098  noetalem1  28107  cutsun12  28185  cofcutrtime  28322  addsuniflem  28396  addbday  28413  negsval  28420  mulsproplem12  28522  mulsproplem13  28523  mulsproplem14  28524  mulsuniflem  28544  mulsass  28561  precsexlem6  28607  precsexlem7  28608  precsexlem10  28611  precsexlem11  28612  ex-ss  31037  shsleji  31981  shsval2i  31998  ssjo  32058  sshhococi  32157  padct  33361  symgcom  33694  cycpmco2lem5  33741  cycpmco2lem6  33742  cycpmco2lem7  33743  cycpmco2  33744  gsumvsca1  33837  gsumvsca2  33838  elrgspnsubrunlem1  33858  rlocbas  33879  rlocaddval  33880  rlocmulval  33881  elrspunsn  34029  mxidlprm  34045  idlsrgbas  34086  idlsrgplusg  34087  idlsrgmulr  34089  fldextrspundgdvdslem  34362  fldextrspundgdvds  34363  constrextdg2lem  34430  esumsplit  34735  esumpad2  34738  aean  34927  sxbrsigalem2  34968  bnj931  35451  tz9.1regs  35870  subfacp1lem2b  36064  subfacp1lem3  36065  subfacp1lem5  36067  kur14lem7  36095  kur14lem9  36097  cvmliftlem10  36177  satfsschain  36247  fmlasssuc  36272  refssfne  37270  filnetlem3  37292  bj-unrab  37963  bj-snglsstag  38018  bj-2upln0  38060  bj-ccssccbar  38275  rdgssun  38438  finixpnum  38665  mbfresfi  38721  prdsbnd  38864  heibor1lem  38880  rrnequiv  38906  paddunssN  41002  sspadd1  41009  sspadd2  41010  pclfinN  41094  dochdmj1  42584  dvhdimlem  42638  elrfi  43842  mzpcompact2lem  43899  eldioph2  43910  eldioph4b  43955  ttac  44180  pwssplit4  44228  pwslnmlem2  44232  isnumbasgrplem2  44243  algbase  44313  algaddg  44314  algmulr  44315  fiuneneq  44331  idomsubgmo  44332  onexlimgt  44382  omabs2  44471  tfsconcatrnss12  44488  rclexi  44752  rtrclex  44754  trclubgNEW  44755  trclexi  44757  rtrclexi  44758  cnvrcl0  44762  cnvtrcl0  44763  dfrtrcl5  44766  trrelsuperrel2dg  44808  dfrcl2  44811  relexp0a  44853  relexpaddss  44855  trclimalb2  44863  frege83d  44885  frege131d  44901  dssmapnvod  45157  clsk3nimkb  45177  isotone1  45185  grumnudlem  45406  dmwf  46091  hfdm  46154  infxrpnf  46592  mccllem  46745  cncfiooicclem1  47039  dvmptfprod  47091  dvnprodlem1  47092  iblsplit  47112  fourierdlem54  47306  fourierdlem102  47354  fourierdlem103  47355  fourierdlem104  47356  fourierdlem114  47366  sge0resplit  47552  sge0split  47555  sge0splitmpt  47557  sge0xaddlem1  47579  isomenndlem  47676  hoiprodp1  47734  hoidmvlelem1  47741  hoidmvlelem2  47742  hoidmvlelem3  47743  hoidmvlelem4  47744  wrddun  48035  chndun  48040  chnrun  48045  dfnbgrss2  49093  gsumsplit2f  49413  parhomssun  50883  elpglem2  51016