Theorem ssun1 3368

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

Syntax hints:   ∨ wo 713   ∈ wcel 2200   ∪ cun 3196   ⊆ wss 3198

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 2802  df-un 3202  df-in 3204  df-ss 3211

This theorem is referenced by:  ssun2  3369  ssun3  3370  elun1  3372  inabs  3437  reuun1  3487  un00  3539  undifabs  3569  undifss  3573  snsspr1  3819  snsstp1  3821  snsstp2  3822  prsstp12  3824  exmidundif  4294  sssucid  4510  unexb  4537  dmexg  4994  fvun1  5708  dftpos2  6422  tpostpos2  6426  ac6sfi  7080  caserel  7277  finomni  7330  ressxr  8213  nnssnn0  9395  un0addcl  9425  un0mulcl  9426  nn0ssxnn0  9458  ccatclab  11161  ccatrn  11176  fsumsplit  11958  fsum2d  11986  fsumabs  12016  fprodsplitdc  12147  fprod2d  12174  ennnfonelemss  13021  prdssca  13348  prdsbas  13349  prdsplusg  13350  prdsmulr  13351  lspun  14406  cnfldbas  14564  mpocnfldadd  14565  mpocnfldmul  14567  cnfldcj  14569  cnfldtset  14570  cnfldle  14571  cnfldds  14572  psrplusgg  14682  dvmptfsum  15439  elplyr  15454  lgsdir2lem3  15749  lgsquadlem2  15797  bdunexb  16451