Metamath Proof Explorer


Definition df-alsi

Description: Define "all some" applied to a top-level implication, which means ps is true whenever ph is true and there is at least one x where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018)

Ref Expression
Assertion df-alsi ∀!xφψxφψxφ

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvarx
1 wph wffφ
2 wps wffψ
3 1 2 0 walsi wff∀!xφψ
4 1 2 wi wffφψ
5 4 0 wal wffxφψ
6 1 0 wex wffxφ
7 5 6 wa wffxφψxφ
8 3 7 wb wff∀!xφψxφψxφ