Theorem ssun1 3776

Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ssun1	|- A C_ ( A u. B )

Proof of Theorem ssun1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		orc 400	. . 3 |- ( x e. A -> ( x e. A \/ x e. B ) )
2		elun 3753	. . 3 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
3	1, 2	sylibr 224	. 2 |- ( x e. A -> x e. ( A u. B ) )
4	3	ssriv 3607	1 |- A C_ ( A u. B )

Syntax hints:   \/ wo 383   e. wcel 1990   u. cun 3572   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588

This theorem is referenced by:  ssun2  3777  ssun3  3778  elun1  3780  inabs  3855  reuun1  3909  un00  4011  snsspr1  4345  snsstp1  4347  snsstp2  4348  uniintsn  4514  sofld  5581  sssucid  5802  fvrn0  6216  ovima0  6813  unexb  6958  dmexg  7097  suppun  7315  dftpos2  7369  tpostpos2  7373  wfrlem14  7428  wfrlem15  7429  tfrlem11  7484  oaabs2  7725  ralxpmap  7907  domss2  8119  mapunen  8129  ac6sfi  8204  frfi  8205  unfir  8228  domunfican  8233  iunfi  8254  elfiun  8336  dffi3  8337  unwdomg  8489  unxpwdom2  8493  unxpwdom  8494  cantnfp1lem1  8575  cantnfp1lem3  8577  tc2  8618  unwf  8673  rankunb  8713  r0weon  8835  infxpenlem  8836  dfac2  8953  cdadom3  9010  cdainflem  9013  infunabs  9029  infcda  9030  infdif  9031  ackbij1lem15  9056  cfsmolem  9092  isfin4-3  9137  fin23lem11  9139  fin1a2lem10  9231  fin1a2lem13  9234  axdc3lem4  9275  axcclem  9279  zornn0g  9327  ttukeylem1  9331  ttukeylem5  9335  ttukeylem7  9337  fingch  9445  fpwwe2lem13  9464  gchac  9503  wunfi  9543  wundm  9550  wunex2  9560  inar1  9597  ressxr  10083  nnssnn0  11295  un0addcl  11326  un0mulcl  11327  nn0ssxnn0  11366  hashbclem  13236  hashf1lem1  13239  hashf1lem2  13240  ccatrn  13372  trclublem  13734  relexpdmg  13782  relexpaddg  13793  fsumsplit  14471  fsum2d  14502  fsumabs  14533  fsumrlim  14543  fsumo1  14544  incexclem  14568  fprodsplit  14696  fprod2d  14711  lcmfunsnlem1  15350  coprmprod  15375  vdwapid1  15679  vdwlem6  15690  ramcl2  15720  isstruct2  15867  srngbase  16009  srngplusg  16010  srngmulr  16011  lmodbase  16018  lmodplusg  16019  lmodsca  16020  ipsbase  16025  ipsaddg  16026  ipsmulr  16027  phlbase  16035  phlplusg  16036  phlsca  16037  odrngbas  16067  odrngplusg  16068  odrngmulr  16069  prdssca  16116  prdsbas  16117  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdsip  16121  prdsle  16122  prdsds  16124  prdstset  16126  imasbas  16172  imasplusg  16177  imasmulr  16178  imassca  16179  imasvsca  16180  imasip  16181  mreexexlem2d  16305  drsdirfi  16938  ipobas  17155  ipotset  17157  acsfiindd  17177  psdmrn  17207  dirdm  17234  gsumzsplit  18327  gsumsplit2  18329  gsumzunsnd  18355  gsum2dlem2  18370  dprdfadd  18419  dmdprdsplit2lem  18444  dmdprdsplit2  18445  dmdprdsplit  18446  dprdsplit  18447  ablfac1eulem  18471  lspun  18987  lspsolv  19143  lsppratlem3  19149  islbs3  19155  lbsextlem2  19159  lbsextlem4  19161  psrbagaddcl  19370  psrbas  19378  psrplusg  19381  psrmulr  19384  mplsubglem  19434  mplcoe1  19465  mplcoe5  19468  cnfldbas  19750  cnfldadd  19751  cnfldmul  19752  cnfldcj  19753  cnfldtset  19754  cnfldle  19755  cnfldds  19756  mdetunilem9  20426  basdif0  20757  ordtbas2  20995  ordtbas  20996  ordtopn1  20998  leordtval2  21016  iocpnfordt  21019  icomnfordt  21020  uncmp  21206  fiuncmp  21207  bwth  21213  locfincmp  21329  comppfsc  21335  1stckgenlem  21356  1stckgen  21357  ptbasin  21380  ptbasfi  21384  dfac14lem  21420  dfac14  21421  ptuncnv  21610  ptunhmeo  21611  ptcmpfi  21616  fbun  21644  trfil2  21691  ufprim  21713  ufileu  21723  filufint  21724  ufildr  21735  fmfnfm  21762  hausflim  21785  fclsfnflim  21831  alexsubALTlem4  21854  tmdgsum  21899  tsmsgsum  21942  tsmsres  21947  tsmssplit  21955  tsmsxplem1  21956  ustssco  22018  ustuqtop1  22045  prdsxmetlem  22173  prdsbl  22296  icccmplem2  22626  fsumcn  22673  cnmpt2pc  22727  rrxmetlem  23190  rrxmet  23191  rrxdstprj1  23192  ovolctb2  23260  ovolunnul  23268  ovolfiniun  23269  nulmbl2  23304  finiunmbl  23312  volfiniun  23315  icombl  23332  ioombl  23333  uniiccdif  23346  mbfres2  23412  itg2splitlem  23515  itg2split  23516  itgfsum  23593  itgsplit  23602  itgsplitioo  23604  dvreslem  23673  dvaddbr  23701  dvmulbr  23702  dvmptfsum  23738  lhop  23779  dvcnvrelem2  23781  mdegcl  23829  elplyr  23957  plyrem  24060  xrlimcnp  24695  fsumharmonic  24738  chtdif  24884  lgsdir2lem3  25052  lgsquadlem2  25106  dchrisum0lem1b  25204  pntrlog2bndlem6  25272  pntlemf  25294  ex-ss  27284  shsleji  28229  shsval2i  28246  ssjo  28306  sshhococi  28405  padct  29497  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  esumsplit  30115  esumpad2  30118  aean  30307  sxbrsigalem2  30348  bnj931  30841  subfacp1lem2b  31163  subfacp1lem3  31164  subfacp1lem5  31166  kur14lem7  31194  kur14lem9  31196  cvmliftlem10  31276  dftrpred3g  31733  scutun12  31917  refssfne  32353  filnetlem3  32375  bj-unrab  32922  bj-snglsstag  32969  bj-2upln0  33011  bj-ccssccbar  33104  finixpnum  33394  matunitlindflem1  33405  mbfresfi  33456  prdsbnd  33592  heibor1lem  33608  rrnequiv  33634  paddunssN  35094  sspadd1  35101  sspadd2  35102  pclfinN  35186  dochdmj1  36679  dvhdimlem  36733  elrfi  37257  mzpcompact2lem  37314  eldioph2  37325  eldioph4b  37375  ttac  37603  pwssplit4  37659  pwslnmlem2  37663  isnumbasgrplem2  37674  algbase  37748  algaddg  37749  algmulr  37750  fiuneneq  37775  idomsubgmo  37776  rclexi  37922  rtrclex  37924  trclubgNEW  37925  trclexi  37927  rtrclexi  37928  cnvrcl0  37932  cnvtrcl0  37933  dfrtrcl5  37936  trrelsuperrel2dg  37963  dfrcl2  37966  relexp0a  38008  relexpaddss  38010  trclimalb2  38018  frege83d  38040  frege131d  38056  dssmapnvod  38314  clsk3nimkb  38338  isotone1  38346  compneOLD  38644  infxrpnf  39674  mccllem  39829  cncfiooicclem1  40106  dvmptfprod  40160  dvnprodlem1  40161  iblsplit  40182  fourierdlem54  40377  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  sge0resplit  40623  sge0split  40626  sge0splitmpt  40628  sge0xaddlem1  40650  isomenndlem  40744  hoiprodp1  40802  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  gsumsplit2f  42143  setrec1lem4  42437  elpglem2  42455