Theorem elssuni 3893

Description: An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)

Assertion

Ref	Expression
elssuni	⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵)

Proof of Theorem elssuni

Step	Hyp	Ref	Expression
1		ssid 3222	. 2 ⊢ 𝐴 ⊆ 𝐴
2		ssuni 3887	. 2 ⊢ ((𝐴 ⊆ 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐴 ⊆ ∪ 𝐵)
3	1, 2	mpan 424	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2178   ⊆ wss 3175  ∪ cuni 3865

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 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2779  df-in 3181  df-ss 3188  df-uni 3866

This theorem is referenced by:  unissel  3894  ssunieq  3898  pwuni  4253  pwel  4281  uniopel  4320  iunpw  4546  dmrnssfld  4961  iotaexab  5270  fvssunirng  5615  relfvssunirn  5616  sefvex  5621  riotaexg  5928  pwuninel2  6393  tfrlem9  6430  tfrexlem  6445  sbthlem1  7087  sbthlem2  7088  unirnioo  10132  eltopss  14642  toponss  14659  isbasis3g  14679  baspartn  14683  bastg  14694  tgcl  14697  epttop  14723  difopn  14741  ssntr  14755  isopn3  14758  isopn3i  14768  neiuni  14794  resttopon  14804  restopn2  14816  ssidcn  14843  lmtopcnp  14883  txuni2  14889  hmeoimaf1o  14947  tgioo  15187  bj-elssuniab  16035