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  10067  eltopss  14353  toponss  14370  isbasis3g  14390  baspartn  14394  bastg  14405  tgcl  14408  epttop  14434  difopn  14452  ssntr  14466  isopn3  14469  isopn3i  14479  neiuni  14505  resttopon  14515  restopn2  14527  ssidcn  14554  lmtopcnp  14594  txuni2  14600  hmeoimaf1o  14658  tgioo  14898  bj-elssuniab  15545