Theorem ssun1 3340

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

Syntax hints:   ∨ wo 710   ∈ wcel 2177   ∪ cun 3168   ⊆ wss 3170

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-in 3176  df-ss 3183

This theorem is referenced by:  ssun2  3341  ssun3  3342  elun1  3344  inabs  3409  reuun1  3459  un00  3511  undifabs  3541  undifss  3545  snsspr1  3787  snsstp1  3789  snsstp2  3790  prsstp12  3792  exmidundif  4258  sssucid  4470  unexb  4497  dmexg  4951  fvun1  5658  dftpos2  6360  tpostpos2  6364  ac6sfi  7010  caserel  7204  finomni  7257  ressxr  8136  nnssnn0  9318  un0addcl  9348  un0mulcl  9349  nn0ssxnn0  9381  ccatclab  11073  ccatrn  11088  fsumsplit  11793  fsum2d  11821  fsumabs  11851  fprodsplitdc  11982  fprod2d  12009  ennnfonelemss  12856  prdssca  13182  prdsbas  13183  prdsplusg  13184  prdsmulr  13185  lspun  14239  cnfldbas  14397  mpocnfldadd  14398  mpocnfldmul  14400  cnfldcj  14402  cnfldtset  14403  cnfldle  14404  cnfldds  14405  psrplusgg  14515  dvmptfsum  15272  elplyr  15287  lgsdir2lem3  15582  lgsquadlem2  15630  bdunexb  15994