Theorem ssun1 3392

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

Syntax hints:   ∨ wo 720   ∈ wcel 2209   ∪ cun 3218   ⊆ wss 3220

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233

This theorem is referenced by:  ssun2  3393  ssun3  3394  elun1  3396  inabs  3463  reuun1  3515  un00  3566  undifabs  3601  undifss  3605  snsspr1  3858  snsstp1  3860  snsstp2  3861  prsstp12  3863  exmidundif  4338  sssucid  4555  unexb  4583  dmexg  5041  fvun1  5763  dftpos2  6522  tpostpos2  6526  mapunen  7141  ac6sfi  7192  caserel  7417  finomni  7470  ressxr  8359  nnssnn0  9545  un0addcl  9575  un0mulcl  9576  nn0ssxnn0  9612  hashfibclem  11260  hashf1lem1  11263  hashf1lem2  11264  ccatclab  11340  ccatrn  11355  fsumsplit  12152  fsum2d  12180  fsumabs  12210  fprodsplitdc  12341  fprod2d  12368  ennnfonelemss  13279  gsump1  14134  gsumzfi  14135  gsumclfi  14136  gsummptfidmadd  14138  gsumsubmclfi  14140  gsumconstcmn  14143  prdssca  14152  prdsbas  14153  prdsplusg  14154  prdsmulr  14155  lspun  14711  cnfldbas  14869  mpocnfldadd  14870  mpocnfldmul  14872  cnfldcj  14874  cnfldtset  14875  cnfldle  14876  cnfldds  14877  gsumfsum  14895  psrplusgg  14992  dvmptfsum  15749  elplyr  15764  lgsdir2lem3  16063  lgsquadlem2  16111  bdunexb  16860