Description: The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | prcssprc | |- ( ( A C_ B /\ A e/ _V ) -> B e/ _V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssexg | |- ( ( A C_ B /\ B e. _V ) -> A e. _V ) |
|
2 | 1 | ex | |- ( A C_ B -> ( B e. _V -> A e. _V ) ) |
3 | 2 | nelcon3d | |- ( A C_ B -> ( A e/ _V -> B e/ _V ) ) |
4 | 3 | imp | |- ( ( A C_ B /\ A e/ _V ) -> B e/ _V ) |