Description: The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | superficl.a | ||
Assertion | superuncl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | superficl.a | ||
2 | vex | ||
3 | vex | ||
4 | 2 3 | unex | |
5 | sseq2 | ||
6 | sseq2 | ||
7 | sseq2 | ||
8 | ssun3 | ||
9 | 8 | adantr | |
10 | 1 4 5 6 7 9 | cllem0 |