Theorem ssun1 4033

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 853	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 4010	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 226	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3858	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 833   ∈ wcel 2048   ∪ cun 3823   ⊆ wss 3825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-un 3830  df-in 3832  df-ss 3839

This theorem is referenced by:  ssun2  4034  ssun3  4035  elun1  4037  difsssymdif  4111  inabs  4114  reuun1  4167  un00  4271  snsspr1  4615  snsstp1  4617  snsstp2  4618  uniintsn  4780  sofld  5878  sssucid  6100  fvrn0  6521  ovima0  7137  unexb  7282  dmexg  7422  suppun  7646  dftpos2  7705  tpostpos2  7709  wfrlem14  7765  wfrlem15  7766  tfrlem11  7821  oaabs2  8064  ralxpmap  8250  domss2  8464  mapunen  8474  ac6sfi  8549  frfi  8550  unfir  8573  domunfican  8578  iunfi  8599  elfiun  8681  dffi3  8682  unwdomg  8835  unxpwdom2  8839  unxpwdom  8840  cantnfp1lem1  8927  cantnfp1lem3  8929  tc2  8970  unwf  9025  rankunb  9065  r0weon  9224  infxpenlem  9225  dfac2b  9342  djudoml  9400  cdainflem  9403  infunabs  9419  infdju  9420  infdif  9421  ackbij1lem15  9446  cfsmolem  9482  isfin4p1  9527  fin23lem11  9529  fin1a2lem10  9621  fin1a2lem13  9624  axdc3lem4  9665  axcclem  9669  zornn0g  9717  ttukeylem1  9721  ttukeylem5  9725  ttukeylem7  9727  fingch  9835  fpwwe2lem13  9854  gchac  9893  wunfi  9933  wundm  9940  wunex2  9950  inar1  9987  ressxr  10476  nnssnn0  11703  un0addcl  11735  un0mulcl  11736  nn0ssxnn0  11775  hashbclem  13613  hashf1lem1  13616  hashf1lem2  13617  ccatrn  13742  trclublem  14206  relexpdmg  14252  relexpaddg  14263  fsumsplit  14947  fsum2d  14976  fsumabs  15006  fsumrlim  15016  fsumo1  15017  incexclem  15041  fprodsplit  15170  fprod2d  15185  lcmfunsnlem1  15827  coprmprod  15851  vdwapid1  16157  vdwlem6  16168  ramcl2  16198  isstruct2  16339  srngbase  16474  srngplusg  16475  srngmulr  16476  lmodbase  16483  lmodplusg  16484  lmodsca  16485  ipsbase  16490  ipsaddg  16491  ipsmulr  16492  phlbase  16500  phlplusg  16501  phlsca  16502  odrngbas  16526  odrngplusg  16527  odrngmulr  16528  prdssca  16575  prdsbas  16576  prdsplusg  16577  prdsmulr  16578  prdsvsca  16579  prdsip  16580  prdsle  16581  prdsds  16583  prdstset  16585  imasbas  16631  imasplusg  16636  imasmulr  16637  imassca  16638  imasvsca  16639  imasip  16640  mreexexlem2d  16764  drsdirfi  17396  ipobas  17613  ipotset  17615  acsfiindd  17635  psdmrn  17665  dirdm  17692  grpinvfval  17919  mulgfval  18003  gsumzsplit  18790  gsumsplit2  18792  gsumzunsnd  18819  gsum2dlem2  18834  dprdfadd  18882  dmdprdsplit2lem  18907  dmdprdsplit2  18908  dmdprdsplit  18909  dprdsplit  18910  ablfac1eulem  18934  lspun  19471  lspsolv  19627  lsppratlem3  19633  islbs3  19639  lbsextlem2  19643  lbsextlem4  19645  psrbagaddcl  19854  psrbas  19862  psrplusg  19865  psrmulr  19868  mplsubglem  19918  mplcoe1  19949  mplcoe5  19952  cnfldbas  20241  cnfldadd  20242  cnfldmul  20243  cnfldcj  20244  cnfldtset  20245  cnfldle  20246  cnfldds  20247  mdetunilem9  20923  basdif0  21255  ordtbas2  21493  ordtbas  21494  ordtopn1  21496  leordtval2  21514  iocpnfordt  21517  icomnfordt  21518  uncmp  21705  fiuncmp  21706  bwth  21712  locfincmp  21828  comppfsc  21834  1stckgenlem  21855  1stckgen  21856  ptbasin  21879  ptbasfi  21883  dfac14lem  21919  dfac14  21920  ptuncnv  22109  ptunhmeo  22110  ptcmpfi  22115  fbun  22142  trfil2  22189  ufprim  22211  ufileu  22221  filufint  22222  ufildr  22233  fmfnfm  22260  hausflim  22283  fclsfnflim  22329  alexsubALTlem4  22352  tmdgsum  22397  tsmsgsum  22440  tsmsres  22445  tsmssplit  22453  tsmsxplem1  22454  ustssco  22516  ustuqtop1  22543  prdsxmetlem  22671  prdsbl  22794  icccmplem2  23124  fsumcn  23171  cnmpopc  23225  rrxmetlem  23703  rrxmet  23704  rrxdstprj1  23705  ovolctb2  23786  ovolunnul  23794  ovolfiniun  23795  nulmbl2  23830  finiunmbl  23838  volfiniun  23841  icombl  23858  ioombl  23859  uniiccdif  23872  mbfres2  23939  itg2splitlem  24042  itg2split  24043  itgfsum  24120  itgsplit  24129  itgsplitioo  24131  dvreslem  24200  dvaddbr  24228  dvmulbr  24229  dvmptfsum  24265  lhop  24306  dvcnvrelem2  24308  mdegcl  24356  elplyr  24484  plyrem  24587  xrlimcnp  25238  fsumharmonic  25281  chtdif  25427  lgsdir2lem3  25595  lgsquadlem2  25649  dchrisum0lem1b  25783  pntrlog2bndlem6  25851  pntlemf  25873  ex-ss  27974  shsleji  28918  shsval2i  28935  ssjo  28995  sshhococi  29094  padct  30196  gsumle  30478  gsumvsca1  30481  gsumvsca2  30482  esumsplit  30913  esumpad2  30916  aean  31105  sxbrsigalem2  31146  bnj931  31651  subfacp1lem2b  31973  subfacp1lem3  31974  subfacp1lem5  31976  kur14lem7  32004  kur14lem9  32006  cvmliftlem10  32086  dftrpred3g  32533  frrlem12  32595  frrlem13  32596  scutun12  32732  refssfne  33167  filnetlem3  33189  bj-unrab  33679  bj-snglsstag  33746  bj-2upln0  33788  bj-ccssccbar  33903  rdgssun  34036  finixpnum  34266  matunitlindflem1  34277  mbfresfi  34327  prdsbnd  34461  heibor1lem  34477  rrnequiv  34503  paddunssN  36337  sspadd1  36344  sspadd2  36345  pclfinN  36429  dochdmj1  37919  dvhdimlem  37973  elrfi  38631  mzpcompact2lem  38688  eldioph2  38699  eldioph4b  38749  ttac  38974  pwssplit4  39030  pwslnmlem2  39034  isnumbasgrplem2  39045  algbase  39119  algaddg  39120  algmulr  39121  fiuneneq  39138  idomsubgmo  39139  rclexi  39283  rtrclex  39285  trclubgNEW  39286  trclexi  39288  rtrclexi  39289  cnvrcl0  39293  cnvtrcl0  39294  dfrtrcl5  39297  trrelsuperrel2dg  39324  dfrcl2  39327  relexp0a  39369  relexpaddss  39371  trclimalb2  39379  frege83d  39401  frege131d  39417  dssmapnvod  39674  clsk3nimkb  39698  isotone1  39706  grumnudlem  39941  compneOLD  40136  infxrpnf  41098  mccllem  41255  cncfiooicclem1  41552  dvmptfprod  41606  dvnprodlem1  41607  iblsplit  41627  fourierdlem54  41822  fourierdlem102  41870  fourierdlem103  41871  fourierdlem104  41872  fourierdlem114  41882  sge0resplit  42065  sge0split  42068  sge0splitmpt  42070  sge0xaddlem1  42092  isomenndlem  42189  hoiprodp1  42247  hoidmvlelem1  42254  hoidmvlelem2  42255  hoidmvlelem3  42256  hoidmvlelem4  42257  gsumsplit2f  43716  setrec1lem4  44100  elpglem2  44121