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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elssuni | |- ( A e. B -> A C_ U. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssid | |- A C_ A |
|
| 2 | ssuni | |- ( ( A C_ A /\ A e. B ) -> A C_ U. B ) |
|
| 3 | 1 2 | mpan | |- ( A e. B -> A C_ U. B ) |