Theorem elssuni 3839

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

Syntax hints:   → wi 4   ∈ wcel 2148   ⊆ wss 3131  ∪ cuni 3811

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-in 3137  df-ss 3144  df-uni 3812

This theorem is referenced by:  unissel  3840  ssunieq  3844  pwuni  4194  pwel  4220  uniopel  4258  iunpw  4482  dmrnssfld  4892  fvssunirng  5532  relfvssunirn  5533  sefvex  5538  riotaexg  5837  pwuninel2  6285  tfrlem9  6322  tfrexlem  6337  sbthlem1  6958  sbthlem2  6959  unirnioo  9975  eltopss  13548  toponss  13565  isbasis3g  13585  baspartn  13589  bastg  13600  tgcl  13603  epttop  13629  difopn  13647  ssntr  13661  isopn3  13664  isopn3i  13674  neiuni  13700  resttopon  13710  restopn2  13722  ssidcn  13749  lmtopcnp  13789  txuni2  13795  hmeoimaf1o  13853  tgioo  14085  bj-elssuniab  14582