Description: Define "all some" applied to a class, which means ph is true for all x in A and there is at least one x in A . (Contributed by David A. Wheeler, 20-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-alsc | |- ( A! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | |- x |
|
| 1 | cA | |- A |
|
| 2 | wph | |- ph |
|
| 3 | 2 0 1 | walsc | |- A! x e. A ph |
| 4 | 2 0 1 | wral | |- A. x e. A ph |
| 5 | 0 | cv | |- x |
| 6 | 5 1 | wcel | |- x e. A |
| 7 | 6 0 | wex | |- E. x x e. A |
| 8 | 4 7 | wa | |- ( A. x e. A ph /\ E. x x e. A ) |
| 9 | 3 8 | wb | |- ( A! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) ) |