Theorem elssuni 3822

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

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

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 3795

This theorem is referenced by:  unissel  3823  ssunieq  3827  pwuni  4176  pwel  4201  uniopel  4239  iunpw  4463  dmrnssfld  4872  fvssunirng  5509  relfvssunirn  5510  sefvex  5515  riotaexg  5811  pwuninel2  6259  tfrlem9  6296  tfrexlem  6311  sbthlem1  6931  sbthlem2  6932  unirnioo  9919  eltopss  12762  toponss  12779  isbasis3g  12799  baspartn  12803  bastg  12816  tgcl  12819  epttop  12845  difopn  12863  ssntr  12877  isopn3  12880  isopn3i  12890  neiuni  12916  resttopon  12926  restopn2  12938  ssidcn  12965  lmtopcnp  13005  txuni2  13011  hmeoimaf1o  13069  tgioo  13301  bj-elssuniab  13787