Theorem ssun1 4106

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

Syntax hints:   ∨ wo 844   ∈ wcel 2106   ∪ cun 3885   ⊆ wss 3887

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904

This theorem is referenced by:  ssun2  4107  ssun3  4108  elun1  4110  difsssymdif  4186  inabs  4189  reuun1  4251  un00  4376  pwunss  4553  pwundif  4559  snsspr1  4747  snsstp1  4749  snsstp2  4750  uniintsn  4918  sofld  6090  sssucid  6343  fvrn0  6802  ovima0  7451  unexb  7598  dmexg  7750  suppun  8000  dftpos2  8059  tpostpos2  8063  frrlem12  8113  frrlem13  8114  wfrlem14OLD  8153  wfrlem15OLD  8154  tfrlem11  8219  oaabs2  8479  ralxpmap  8684  domss2  8923  mapunen  8933  ac6sfi  9058  frfi  9059  unfir  9082  domunfican  9087  iunfi  9107  elfiun  9189  dffi3  9190  unwdomg  9343  unxpwdom2  9347  unxpwdom  9348  cantnfp1lem1  9436  cantnfp1lem3  9438  tc2  9500  unwf  9568  rankunb  9608  r0weon  9768  infxpenlem  9769  dfac2b  9886  djudoml  9940  cdainflem  9943  infunabs  9963  infdju  9964  infdif  9965  ackbij1lem15  9990  cfsmolem  10026  isfin4p1  10071  fin23lem11  10073  fin1a2lem10  10165  fin1a2lem13  10168  axdc3lem4  10209  axcclem  10213  zornn0g  10261  ttukeylem1  10265  ttukeylem5  10269  ttukeylem7  10271  fingch  10379  fpwwe2lem12  10398  gchac  10437  wunfi  10477  wundm  10484  wunex2  10494  inar1  10531  ressxr  11019  nnssnn0  12236  un0addcl  12266  un0mulcl  12267  nn0ssxnn0  12308  hashbclem  14164  hashf1lem1  14168  hashf1lem1OLD  14169  hashf1lem2  14170  ccatrn  14294  trclublem  14706  relexpdmg  14753  relexpaddg  14764  fsumsplit  15453  fsum2d  15483  fsumabs  15513  fsumrlim  15523  fsumo1  15524  incexclem  15548  fprodsplit  15676  fprod2d  15691  lcmfunsnlem1  16342  coprmprod  16366  vdwapid1  16676  vdwlem6  16687  ramcl2  16717  isstruct2  16850  srngbase  17020  srngplusg  17021  srngmulr  17022  lmodbase  17036  lmodplusg  17037  lmodsca  17038  ipsbase  17047  ipsaddg  17048  ipsmulr  17049  phlbase  17057  phlplusg  17058  phlsca  17059  odrngbas  17114  odrngplusg  17115  odrngmulr  17116  prdssca  17167  prdsbas  17168  prdsplusg  17169  prdsmulr  17170  prdsvsca  17171  prdsip  17172  prdsle  17173  prdsds  17175  prdstset  17177  imasbas  17223  imasplusg  17228  imasmulr  17229  imassca  17230  imasvsca  17231  imasip  17232  mreexexlem2d  17354  drsdirfi  18023  ipobas  18249  ipotset  18251  acsfiindd  18271  psdmrn  18291  dirdm  18318  grpinvfval  18618  mulgfval  18702  gsumzsplit  19528  gsumsplit2  19530  gsumzunsnd  19557  gsum2dlem2  19572  dprdfadd  19623  dmdprdsplit2lem  19648  dmdprdsplit2  19649  dmdprdsplit  19650  dprdsplit  19651  ablfac1eulem  19675  lspun  20249  lspsolv  20405  lsppratlem3  20411  islbs3  20417  lbsextlem2  20421  lbsextlem4  20423  cnfldbas  20601  cnfldadd  20602  cnfldmul  20603  cnfldcj  20604  cnfldtset  20605  cnfldle  20606  cnfldds  20607  psrbagaddclOLD  21132  psrbas  21147  psrplusg  21150  psrmulr  21153  mplsubglem  21205  mplcoe1  21238  mplcoe5  21241  mdetunilem9  21769  basdif0  22103  ordtbas2  22342  ordtbas  22343  ordtopn1  22345  leordtval2  22363  iocpnfordt  22366  icomnfordt  22367  uncmp  22554  fiuncmp  22555  bwth  22561  locfincmp  22677  comppfsc  22683  1stckgenlem  22704  1stckgen  22705  ptbasin  22728  ptbasfi  22732  dfac14lem  22768  dfac14  22769  ptuncnv  22958  ptunhmeo  22959  ptcmpfi  22964  fbun  22991  trfil2  23038  ufprim  23060  ufileu  23070  filufint  23071  ufildr  23082  fmfnfm  23109  hausflim  23132  fclsfnflim  23178  alexsubALTlem4  23201  tmdgsum  23246  tsmsgsum  23290  tsmsres  23295  tsmssplit  23303  tsmsxplem1  23304  ustssco  23366  ustuqtop1  23393  prdsxmetlem  23521  prdsbl  23647  icccmplem2  23986  fsumcn  24033  cnmpopc  24091  rrxmetlem  24571  rrxmet  24572  rrxdstprj1  24573  ovolctb2  24656  ovolunnul  24664  ovolfiniun  24665  nulmbl2  24700  finiunmbl  24708  volfiniun  24711  icombl  24728  ioombl  24729  uniiccdif  24742  mbfres2  24809  itg2splitlem  24913  itg2split  24914  itgfsum  24991  itgsplit  25000  itgsplitioo  25002  dvreslem  25073  dvaddbr  25102  dvmulbr  25103  dvmptfsum  25139  lhop  25180  dvcnvrelem2  25182  mdegcl  25234  elplyr  25362  plyrem  25465  xrlimcnp  26118  fsumharmonic  26161  chtdif  26307  lgsdir2lem3  26475  lgsquadlem2  26529  dchrisum0lem1b  26663  pntrlog2bndlem6  26731  pntlemf  26753  ex-ss  28791  shsleji  29732  shsval2i  29749  ssjo  29809  sshhococi  29908  padct  31054  gsumle  31350  symgcom  31352  cycpmco2lem5  31397  cycpmco2lem6  31398  cycpmco2lem7  31399  cycpmco2  31400  gsumvsca1  31479  gsumvsca2  31480  mxidlprm  31640  idlsrgbas  31649  idlsrgplusg  31650  idlsrgmulr  31652  esumsplit  32021  esumpad2  32024  aean  32212  sxbrsigalem2  32253  bnj931  32750  subfacp1lem2b  33143  subfacp1lem3  33144  subfacp1lem5  33146  kur14lem7  33174  kur14lem9  33176  cvmliftlem10  33256  satfsschain  33326  fmlasssuc  33351  xpord2ind  33794  xpord3ind  33800  nosupinfsep  33935  noetalem1  33944  scutun12  34004  cofcutrtime  34093  negsval  34123  refssfne  34547  filnetlem3  34569  bj-unrab  35114  bj-snglsstag  35171  bj-2upln0  35213  bj-ccssccbar  35388  rdgssun  35549  finixpnum  35762  matunitlindflem1  35773  mbfresfi  35823  prdsbnd  35951  heibor1lem  35967  rrnequiv  35993  paddunssN  37822  sspadd1  37829  sspadd2  37830  pclfinN  37914  dochdmj1  39404  dvhdimlem  39458  elrfi  40516  mzpcompact2lem  40573  eldioph2  40584  eldioph4b  40633  ttac  40858  pwssplit4  40914  pwslnmlem2  40918  isnumbasgrplem2  40929  algbase  41003  algaddg  41004  algmulr  41005  fiuneneq  41022  idomsubgmo  41023  rclexi  41223  rtrclex  41225  trclubgNEW  41226  trclexi  41228  rtrclexi  41229  cnvrcl0  41233  cnvtrcl0  41234  dfrtrcl5  41237  trrelsuperrel2dg  41279  dfrcl2  41282  relexp0a  41324  relexpaddss  41326  trclimalb2  41334  frege83d  41356  frege131d  41372  dssmapnvod  41628  clsk3nimkb  41650  isotone1  41658  grumnudlem  41903  infxrpnf  42986  mccllem  43138  cncfiooicclem1  43434  dvmptfprod  43486  dvnprodlem1  43487  iblsplit  43507  fourierdlem54  43701  fourierdlem102  43749  fourierdlem103  43750  fourierdlem104  43751  fourierdlem114  43761  sge0resplit  43944  sge0split  43947  sge0splitmpt  43949  sge0xaddlem1  43971  isomenndlem  44068  hoiprodp1  44126  hoidmvlelem1  44133  hoidmvlelem2  44134  hoidmvlelem3  44135  hoidmvlelem4  44136  gsumsplit2f  45374  setrec1lem4  46396  elpglem2  46417