Theorem elssuni 3863

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

Syntax hints:   → wi 4   ∈ wcel 2164   ⊆ wss 3153  ∪ cuni 3835

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3159  df-ss 3166  df-uni 3836

This theorem is referenced by:  unissel  3864  ssunieq  3868  pwuni  4221  pwel  4247  uniopel  4285  iunpw  4511  dmrnssfld  4925  iotaexab  5233  fvssunirng  5569  relfvssunirn  5570  sefvex  5575  riotaexg  5877  pwuninel2  6335  tfrlem9  6372  tfrexlem  6387  sbthlem1  7016  sbthlem2  7017  unirnioo  10039  eltopss  14177  toponss  14194  isbasis3g  14214  baspartn  14218  bastg  14229  tgcl  14232  epttop  14258  difopn  14276  ssntr  14290  isopn3  14293  isopn3i  14303  neiuni  14329  resttopon  14339  restopn2  14351  ssidcn  14378  lmtopcnp  14418  txuni2  14424  hmeoimaf1o  14482  tgioo  14714  bj-elssuniab  15283