Theorem elssuni 3926

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

Syntax hints:   → wi 4   ∈ wcel 2202   ⊆ wss 3201  ∪ cuni 3898

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-in 3207  df-ss 3214  df-uni 3899

This theorem is referenced by:  unissel  3927  ssunieq  3931  pwuni  4288  pwel  4316  uniopel  4355  iunpw  4583  dmrnssfld  5001  iotaexab  5312  fvssunirng  5663  relfvssunirn  5664  sefvex  5669  riotaexg  5985  pwuninel2  6491  tfrlem9  6528  tfrexlem  6543  sbthlem1  7199  sbthlem2  7200  unirnioo  10251  eltopss  14800  toponss  14817  isbasis3g  14837  baspartn  14841  bastg  14852  tgcl  14855  epttop  14881  difopn  14899  ssntr  14913  isopn3  14916  isopn3i  14926  neiuni  14952  resttopon  14962  restopn2  14974  ssidcn  15001  lmtopcnp  15041  txuni2  15047  hmeoimaf1o  15105  tgioo  15345  bj-elssuniab  16489