Mathbox for David A. Wheeler |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-alsi | Structured version Visualization version GIF version |
Description: Define "all some" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true and there is at least one 𝑥 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.) |
Ref | Expression |
---|---|
df-alsi | ⊢ (∀!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | vx | . . 3 setvar 𝑥 | |
4 | 1, 2, 3 | walsi 46190 | . 2 wff ∀!𝑥(𝜑 → 𝜓) |
5 | 1, 2 | wi 4 | . . . 4 wff (𝜑 → 𝜓) |
6 | 5, 3 | wal 1541 | . . 3 wff ∀𝑥(𝜑 → 𝜓) |
7 | 1, 3 | wex 1787 | . . 3 wff ∃𝑥𝜑 |
8 | 6, 7 | wa 399 | . 2 wff (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑) |
9 | 4, 8 | wb 209 | 1 wff (∀!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: alsconv 46194 alsi1d 46195 alsi2d 46196 alsi-no-surprise 46200 |
Copyright terms: Public domain | W3C validator |