Theorem elssuni 3868

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

Syntax hints:   → wi 4   ∈ wcel 2167   ⊆ wss 3157  ∪ cuni 3840

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170  df-uni 3841

This theorem is referenced by:  unissel  3869  ssunieq  3873  pwuni  4226  pwel  4252  uniopel  4290  iunpw  4516  dmrnssfld  4930  iotaexab  5238  fvssunirng  5576  relfvssunirn  5577  sefvex  5582  riotaexg  5884  pwuninel2  6349  tfrlem9  6386  tfrexlem  6401  sbthlem1  7032  sbthlem2  7033  unirnioo  10065  eltopss  14329  toponss  14346  isbasis3g  14366  baspartn  14370  bastg  14381  tgcl  14384  epttop  14410  difopn  14428  ssntr  14442  isopn3  14445  isopn3i  14455  neiuni  14481  resttopon  14491  restopn2  14503  ssidcn  14530  lmtopcnp  14570  txuni2  14576  hmeoimaf1o  14634  tgioo  14874  bj-elssuniab  15521