MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssun1 Structured version   Visualization version   GIF version

Theorem ssun1 4145
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.
StepHypRef Expression
1 orc 861 . . 3 (𝑥𝐴 → (𝑥𝐴𝑥𝐵))
2 elun 4122 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
31, 2sylibr 235 . 2 (𝑥𝐴𝑥 ∈ (𝐴𝐵))
43ssriv 3968 1 𝐴 ⊆ (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 841  wcel 2105  cun 3931  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949
This theorem is referenced by:  ssun2  4146  ssun3  4147  elun1  4149  difsssymdif  4226  inabs  4229  reuun1  4282  un00  4390  snsspr1  4739  snsstp1  4741  snsstp2  4742  uniintsn  4904  pwunss  5446  pwundif  5449  sofld  6037  sssucid  6261  fvrn0  6691  ovima0  7316  unexb  7460  dmexg  7602  suppun  7839  dftpos2  7898  tpostpos2  7902  wfrlem14  7957  wfrlem15  7958  tfrlem11  8013  oaabs2  8261  ralxpmap  8448  domss2  8664  mapunen  8674  ac6sfi  8750  frfi  8751  unfir  8774  domunfican  8779  iunfi  8800  elfiun  8882  dffi3  8883  unwdomg  9036  unxpwdom2  9040  unxpwdom  9041  cantnfp1lem1  9129  cantnfp1lem3  9131  tc2  9172  unwf  9227  rankunb  9267  r0weon  9426  infxpenlem  9427  dfac2b  9544  djudoml  9598  cdainflem  9601  infunabs  9617  infdju  9618  infdif  9619  ackbij1lem15  9644  cfsmolem  9680  isfin4p1  9725  fin23lem11  9727  fin1a2lem10  9819  fin1a2lem13  9822  axdc3lem4  9863  axcclem  9867  zornn0g  9915  ttukeylem1  9919  ttukeylem5  9923  ttukeylem7  9925  fingch  10033  fpwwe2lem13  10052  gchac  10091  wunfi  10131  wundm  10138  wunex2  10148  inar1  10185  ressxr  10673  nnssnn0  11888  un0addcl  11918  un0mulcl  11919  nn0ssxnn0  11958  hashbclem  13798  hashf1lem1  13801  hashf1lem2  13802  ccatrn  13931  trclublem  14343  relexpdmg  14389  relexpaddg  14400  fsumsplit  15085  fsum2d  15114  fsumabs  15144  fsumrlim  15154  fsumo1  15155  incexclem  15179  fprodsplit  15308  fprod2d  15323  lcmfunsnlem1  15969  coprmprod  15993  vdwapid1  16299  vdwlem6  16310  ramcl2  16340  isstruct2  16481  srngbase  16616  srngplusg  16617  srngmulr  16618  lmodbase  16625  lmodplusg  16626  lmodsca  16627  ipsbase  16632  ipsaddg  16633  ipsmulr  16634  phlbase  16642  phlplusg  16643  phlsca  16644  odrngbas  16668  odrngplusg  16669  odrngmulr  16670  prdssca  16717  prdsbas  16718  prdsplusg  16719  prdsmulr  16720  prdsvsca  16721  prdsip  16722  prdsle  16723  prdsds  16725  prdstset  16727  imasbas  16773  imasplusg  16778  imasmulr  16779  imassca  16780  imasvsca  16781  imasip  16782  mreexexlem2d  16904  drsdirfi  17536  ipobas  17753  ipotset  17755  acsfiindd  17775  psdmrn  17805  dirdm  17832  grpinvfval  18080  mulgfval  18164  gsumzsplit  18976  gsumsplit2  18978  gsumzunsnd  19005  gsum2dlem2  19020  dprdfadd  19071  dmdprdsplit2lem  19096  dmdprdsplit2  19097  dmdprdsplit  19098  dprdsplit  19099  ablfac1eulem  19123  lspun  19688  lspsolv  19844  lsppratlem3  19850  islbs3  19856  lbsextlem2  19860  lbsextlem4  19862  psrbagaddcl  20078  psrbas  20086  psrplusg  20089  psrmulr  20092  mplsubglem  20142  mplcoe1  20174  mplcoe5  20177  cnfldbas  20477  cnfldadd  20478  cnfldmul  20479  cnfldcj  20480  cnfldtset  20481  cnfldle  20482  cnfldds  20483  mdetunilem9  21157  basdif0  21489  ordtbas2  21727  ordtbas  21728  ordtopn1  21730  leordtval2  21748  iocpnfordt  21751  icomnfordt  21752  uncmp  21939  fiuncmp  21940  bwth  21946  locfincmp  22062  comppfsc  22068  1stckgenlem  22089  1stckgen  22090  ptbasin  22113  ptbasfi  22117  dfac14lem  22153  dfac14  22154  ptuncnv  22343  ptunhmeo  22344  ptcmpfi  22349  fbun  22376  trfil2  22423  ufprim  22445  ufileu  22455  filufint  22456  ufildr  22467  fmfnfm  22494  hausflim  22517  fclsfnflim  22563  alexsubALTlem4  22586  tmdgsum  22631  tsmsgsum  22674  tsmsres  22679  tsmssplit  22687  tsmsxplem1  22688  ustssco  22750  ustuqtop1  22777  prdsxmetlem  22905  prdsbl  23028  icccmplem2  23358  fsumcn  23405  cnmpopc  23459  rrxmetlem  23937  rrxmet  23938  rrxdstprj1  23939  ovolctb2  24020  ovolunnul  24028  ovolfiniun  24029  nulmbl2  24064  finiunmbl  24072  volfiniun  24075  icombl  24092  ioombl  24093  uniiccdif  24106  mbfres2  24173  itg2splitlem  24276  itg2split  24277  itgfsum  24354  itgsplit  24363  itgsplitioo  24365  dvreslem  24434  dvaddbr  24462  dvmulbr  24463  dvmptfsum  24499  lhop  24540  dvcnvrelem2  24542  mdegcl  24590  elplyr  24718  plyrem  24821  xrlimcnp  25473  fsumharmonic  25516  chtdif  25662  lgsdir2lem3  25830  lgsquadlem2  25884  dchrisum0lem1b  26018  pntrlog2bndlem6  26086  pntlemf  26108  ex-ss  28133  shsleji  29074  shsval2i  29091  ssjo  29151  sshhococi  29250  padct  30381  gsumle  30652  symgcom  30654  cycpmco2lem5  30699  cycpmco2lem6  30700  cycpmco2lem7  30701  cycpmco2  30702  gsumvsca1  30781  gsumvsca2  30782  esumsplit  31211  esumpad2  31214  aean  31402  sxbrsigalem2  31443  bnj931  31941  subfacp1lem2b  32325  subfacp1lem3  32326  subfacp1lem5  32328  kur14lem7  32356  kur14lem9  32358  cvmliftlem10  32438  satfsschain  32508  fmlasssuc  32533  dftrpred3g  32969  frrlem12  33031  frrlem13  33032  scutun12  33168  refssfne  33603  filnetlem3  33625  bj-unrab  34141  bj-snglsstag  34190  bj-2upln0  34232  bj-ccssccbar  34391  rdgssun  34541  finixpnum  34758  matunitlindflem1  34769  mbfresfi  34819  prdsbnd  34952  heibor1lem  34968  rrnequiv  34994  paddunssN  36824  sspadd1  36831  sspadd2  36832  pclfinN  36916  dochdmj1  38406  dvhdimlem  38460  elrfi  39169  mzpcompact2lem  39226  eldioph2  39237  eldioph4b  39286  ttac  39511  pwssplit4  39567  pwslnmlem2  39571  isnumbasgrplem2  39582  algbase  39656  algaddg  39657  algmulr  39658  fiuneneq  39675  idomsubgmo  39676  rclexi  39853  rtrclex  39855  trclubgNEW  39856  trclexi  39858  rtrclexi  39859  cnvrcl0  39863  cnvtrcl0  39864  dfrtrcl5  39867  trrelsuperrel2dg  39894  dfrcl2  39897  relexp0a  39939  relexpaddss  39941  trclimalb2  39949  frege83d  39971  frege131d  39987  dssmapnvod  40244  clsk3nimkb  40268  isotone1  40276  grumnudlem  40498  infxrpnf  41597  mccllem  41754  cncfiooicclem1  42052  dvmptfprod  42106  dvnprodlem1  42107  iblsplit  42127  fourierdlem54  42322  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem114  42382  sge0resplit  42565  sge0split  42568  sge0splitmpt  42570  sge0xaddlem1  42592  isomenndlem  42689  hoiprodp1  42747  hoidmvlelem1  42754  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvlelem4  42757  gsumsplit2f  43964  setrec1lem4  44721  elpglem2  44742
  Copyright terms: Public domain W3C validator