Description: If something is true for all then it's true for some class. (Contributed by Stanislas Polu, 9-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rspcdvinvd.1 | |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) |
|
rspcdvinvd.2 | |- ( ph -> A e. B ) |
||
rspcdvinvd.3 | |- ( ph -> A. x e. B ps ) |
||
Assertion | rspcdvinvd | |- ( ph -> ch ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspcdvinvd.1 | |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) |
|
2 | rspcdvinvd.2 | |- ( ph -> A e. B ) |
|
3 | rspcdvinvd.3 | |- ( ph -> A. x e. B ps ) |
|
4 | 2 1 | rspcdv | |- ( ph -> ( A. x e. B ps -> ch ) ) |
5 | 3 4 | mpd | |- ( ph -> ch ) |