Theorem ssun1 3367

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 717	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 3345	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 134	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3228	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 713   ∈ wcel 2200   ∪ cun 3195   ⊆ wss 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210

This theorem is referenced by:  ssun2  3368  ssun3  3369  elun1  3371  inabs  3436  reuun1  3486  un00  3538  undifabs  3568  undifss  3572  snsspr1  3815  snsstp1  3817  snsstp2  3818  prsstp12  3820  exmidundif  4289  sssucid  4505  unexb  4532  dmexg  4987  fvun1  5699  dftpos2  6405  tpostpos2  6409  ac6sfi  7056  caserel  7250  finomni  7303  ressxr  8186  nnssnn0  9368  un0addcl  9398  un0mulcl  9399  nn0ssxnn0  9431  ccatclab  11124  ccatrn  11139  fsumsplit  11913  fsum2d  11941  fsumabs  11971  fprodsplitdc  12102  fprod2d  12129  ennnfonelemss  12976  prdssca  13303  prdsbas  13304  prdsplusg  13305  prdsmulr  13306  lspun  14360  cnfldbas  14518  mpocnfldadd  14519  mpocnfldmul  14521  cnfldcj  14523  cnfldtset  14524  cnfldle  14525  cnfldds  14526  psrplusgg  14636  dvmptfsum  15393  elplyr  15408  lgsdir2lem3  15703  lgsquadlem2  15751  bdunexb  16241