Theorem elssuni 3941

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

Syntax hints:   → wi 4   ∈ wcel 2203   ⊆ wss 3210  ∪ cuni 3913

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-in 3216  df-ss 3223  df-uni 3914

This theorem is referenced by:  unissel  3942  ssunieq  3946  pwuni  4304  pwel  4333  uniopel  4372  iunpw  4600  dmrnssfld  5019  iotaexab  5330  fvssunirng  5684  relfvssunirn  5685  sefvex  5690  riotaexg  6006  pwuninel2  6512  tfrlem9  6549  tfrexlem  6564  sbthlem1  7226  sbthlem2  7227  unirnioo  10305  eltopss  14866  toponss  14883  isbasis3g  14903  baspartn  14907  bastg  14918  tgcl  14921  epttop  14947  difopn  14965  ssntr  14979  isopn3  14982  isopn3i  14992  neiuni  15018  resttopon  15028  restopn2  15040  ssidcn  15067  lmtopcnp  15107  txuni2  15113  hmeoimaf1o  15171  tgioo  15411  bj-elssuniab  16555