Theorem elssuni 3824

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 3167	. 2 ⊢ 𝐴 ⊆ 𝐴
2		ssuni 3818	. 2 ⊢ ((𝐴 ⊆ 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐴 ⊆ ∪ 𝐵)
3	1, 2	mpan 422	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3121  ∪ cuni 3796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134  df-uni 3797

This theorem is referenced by:  unissel  3825  ssunieq  3829  pwuni  4178  pwel  4203  uniopel  4241  iunpw  4465  dmrnssfld  4874  fvssunirng  5511  relfvssunirn  5512  sefvex  5517  riotaexg  5813  pwuninel2  6261  tfrlem9  6298  tfrexlem  6313  sbthlem1  6934  sbthlem2  6935  unirnioo  9930  eltopss  12801  toponss  12818  isbasis3g  12838  baspartn  12842  bastg  12855  tgcl  12858  epttop  12884  difopn  12902  ssntr  12916  isopn3  12919  isopn3i  12929  neiuni  12955  resttopon  12965  restopn2  12977  ssidcn  13004  lmtopcnp  13044  txuni2  13050  hmeoimaf1o  13108  tgioo  13340  bj-elssuniab  13826