Description: Deduction rule: Given "all some" applied to a class, the class is not the empty set. (Contributed by David A. Wheeler, 23-Oct-2018) (Revised by David A. Wheeler, 12-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ralsn0d.1 | |- ( ph -> AE x e. A ( ps -> ch ) ) |
|
| Assertion | ralsn0d | |- ( ph -> A =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralsn0d.1 | |- ( ph -> AE x e. A ( ps -> ch ) ) |
|
| 2 | 1 | rals2d | |- ( ph -> E. x e. A ps ) |
| 3 | rexn0 | |- ( E. x e. A ps -> A =/= (/) ) |
|
| 4 | 2 3 | syl | |- ( ph -> A =/= (/) ) |