Theorem ssun1 4173

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

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

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 3954  df-in 3956  df-ss 3966

This theorem is referenced by:  ssun2  4174  ssun3  4175  elun1  4177  difsssymdif  4253  inabs  4256  reuun1  4318  un00  4443  pwunss  4621  pwundif  4627  snsspr1  4818  snsstp1  4820  snsstp2  4821  uniintsn  4992  sofld  6187  sssucid  6445  fvrn0  6922  ovima0  7586  unexb  7735  dmexg  7894  xpord2indlem  8133  xpord3inddlem  8140  suppun  8169  dftpos2  8228  tpostpos2  8232  frrlem12  8282  frrlem13  8283  wfrlem14OLD  8322  wfrlem15OLD  8323  tfrlem11  8388  oaabs2  8648  ralxpmap  8890  domss2  9136  mapunen  9146  ac6sfi  9287  frfi  9288  unfir  9314  domunfican  9320  iunfi  9340  elfiun  9425  dffi3  9426  unwdomg  9579  unxpwdom2  9583  unxpwdom  9584  cantnfp1lem1  9673  cantnfp1lem3  9675  tc2  9737  unwf  9805  rankunb  9845  r0weon  10007  infxpenlem  10008  dfac2b  10125  djudoml  10179  cdainflem  10182  infunabs  10202  infdju  10203  infdif  10204  ackbij1lem15  10229  cfsmolem  10265  isfin4p1  10310  fin23lem11  10312  fin1a2lem10  10404  fin1a2lem13  10407  axdc3lem4  10448  axcclem  10452  zornn0g  10500  ttukeylem1  10504  ttukeylem5  10508  ttukeylem7  10510  fingch  10618  fpwwe2lem12  10637  gchac  10676  wunfi  10716  wundm  10723  wunex2  10733  inar1  10770  ressxr  11258  nnssnn0  12475  un0addcl  12505  un0mulcl  12506  nn0ssxnn0  12547  hashbclem  14411  hashf1lem1  14415  hashf1lem1OLD  14416  hashf1lem2  14417  ccatrn  14539  trclublem  14942  relexpdmg  14989  relexpaddg  15000  fsumsplit  15687  fsum2d  15717  fsumabs  15747  fsumrlim  15757  fsumo1  15758  incexclem  15782  fprodsplit  15910  fprod2d  15925  lcmfunsnlem1  16574  coprmprod  16598  vdwapid1  16908  vdwlem6  16919  ramcl2  16949  isstruct2  17082  srngbase  17255  srngplusg  17256  srngmulr  17257  lmodbase  17271  lmodplusg  17272  lmodsca  17273  ipsbase  17282  ipsaddg  17283  ipsmulr  17284  phlbase  17292  phlplusg  17293  phlsca  17294  odrngbas  17349  odrngplusg  17350  odrngmulr  17351  prdssca  17402  prdsbas  17403  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  prdsip  17407  prdsle  17408  prdsds  17410  prdstset  17412  imasbas  17458  imasplusg  17463  imasmulr  17464  imassca  17465  imasvsca  17466  imasip  17467  mreexexlem2d  17589  drsdirfi  18258  ipobas  18484  ipotset  18486  acsfiindd  18506  psdmrn  18526  dirdm  18553  grpinvfval  18863  mulgfval  18952  gsumzsplit  19795  gsumsplit2  19797  gsumzunsnd  19824  gsum2dlem2  19839  dprdfadd  19890  dmdprdsplit2lem  19915  dmdprdsplit2  19916  dmdprdsplit  19917  dprdsplit  19918  ablfac1eulem  19942  lspun  20598  lspsolv  20756  lsppratlem3  20762  islbs3  20768  lbsextlem2  20772  lbsextlem4  20774  cnfldbas  20948  cnfldadd  20949  cnfldmul  20950  cnfldcj  20951  cnfldtset  20952  cnfldle  20953  cnfldds  20954  psrbagaddclOLD  21482  psrbas  21497  psrplusg  21500  psrmulr  21503  mplsubglem  21558  mplcoe1  21592  mplcoe5  21595  mdetunilem9  22122  basdif0  22456  ordtbas2  22695  ordtbas  22696  ordtopn1  22698  leordtval2  22716  iocpnfordt  22719  icomnfordt  22720  uncmp  22907  fiuncmp  22908  bwth  22914  locfincmp  23030  comppfsc  23036  1stckgenlem  23057  1stckgen  23058  ptbasin  23081  ptbasfi  23085  dfac14lem  23121  dfac14  23122  ptuncnv  23311  ptunhmeo  23312  ptcmpfi  23317  fbun  23344  trfil2  23391  ufprim  23413  ufileu  23423  filufint  23424  ufildr  23435  fmfnfm  23462  hausflim  23485  fclsfnflim  23531  alexsubALTlem4  23554  tmdgsum  23599  tsmsgsum  23643  tsmsres  23648  tsmssplit  23656  tsmsxplem1  23657  ustssco  23719  ustuqtop1  23746  prdsxmetlem  23874  prdsbl  24000  icccmplem2  24339  fsumcn  24386  cnmpopc  24444  rrxmetlem  24924  rrxmet  24925  rrxdstprj1  24926  ovolctb2  25009  ovolunnul  25017  ovolfiniun  25018  nulmbl2  25053  finiunmbl  25061  volfiniun  25064  icombl  25081  ioombl  25082  uniiccdif  25095  mbfres2  25162  itg2splitlem  25266  itg2split  25267  itgfsum  25344  itgsplit  25353  itgsplitioo  25355  dvreslem  25426  dvaddbr  25455  dvmulbr  25456  dvmptfsum  25492  lhop  25533  dvcnvrelem2  25535  mdegcl  25587  elplyr  25715  plyrem  25818  xrlimcnp  26473  fsumharmonic  26516  chtdif  26662  lgsdir2lem3  26830  lgsquadlem2  26884  dchrisum0lem1b  27018  pntrlog2bndlem6  27086  pntlemf  27108  nosupinfsep  27235  noetalem1  27244  scutun12  27311  cofcutrtime  27414  addsuniflem  27484  negsval  27500  mulsproplem12  27583  mulsproplem13  27584  mulsproplem14  27585  mulsuniflem  27604  mulsass  27621  precsexlem6  27658  precsexlem7  27659  precsexlem10  27662  precsexlem11  27663  ex-ss  29680  shsleji  30623  shsval2i  30640  ssjo  30700  sshhococi  30799  padct  31944  gsumle  32242  symgcom  32244  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmco2  32292  gsumvsca1  32371  gsumvsca2  32372  elrspunsn  32547  mxidlprm  32586  idlsrgbas  32618  idlsrgplusg  32619  idlsrgmulr  32621  esumsplit  33051  esumpad2  33054  aean  33242  sxbrsigalem2  33285  bnj931  33781  subfacp1lem2b  34172  subfacp1lem3  34173  subfacp1lem5  34175  kur14lem7  34203  kur14lem9  34205  cvmliftlem10  34285  satfsschain  34355  fmlasssuc  34380  gg-dvmulbr  35175  refssfne  35243  filnetlem3  35265  bj-unrab  35806  bj-snglsstag  35862  bj-2upln0  35904  bj-ccssccbar  36098  rdgssun  36259  finixpnum  36473  matunitlindflem1  36484  mbfresfi  36534  prdsbnd  36661  heibor1lem  36677  rrnequiv  36703  paddunssN  38679  sspadd1  38686  sspadd2  38687  pclfinN  38771  dochdmj1  40261  dvhdimlem  40315  elrfi  41432  mzpcompact2lem  41489  eldioph2  41500  eldioph4b  41549  ttac  41775  pwssplit4  41831  pwslnmlem2  41835  isnumbasgrplem2  41846  algbase  41920  algaddg  41921  algmulr  41922  fiuneneq  41939  idomsubgmo  41940  onexlimgt  41992  omabs2  42082  tfsconcatrnss12  42099  rclexi  42366  rtrclex  42368  trclubgNEW  42369  trclexi  42371  rtrclexi  42372  cnvrcl0  42376  cnvtrcl0  42377  dfrtrcl5  42380  trrelsuperrel2dg  42422  dfrcl2  42425  relexp0a  42467  relexpaddss  42469  trclimalb2  42477  frege83d  42499  frege131d  42515  dssmapnvod  42771  clsk3nimkb  42791  isotone1  42799  grumnudlem  43044  infxrpnf  44156  mccllem  44313  cncfiooicclem1  44609  dvmptfprod  44661  dvnprodlem1  44662  iblsplit  44682  fourierdlem54  44876  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem114  44936  sge0resplit  45122  sge0split  45125  sge0splitmpt  45127  sge0xaddlem1  45149  isomenndlem  45246  hoiprodp1  45304  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  gsumsplit2f  46590  setrec1lem4  47735  elpglem2  47757