Description: A transformation of
quantifiers and logical connectives. The general
statement that equs3 1760 proves.
This and the following theorems are the general instances of already
proved theorems. They could be moved to the main part, before ax-5 1727.
I
propose to move to the main part: bj-exnalimn 30798, bj-exaleximi 30801,
bj-exalimi 30802, bj-ax12i 30803, bj-ax12wlem 30805. A new label is needed for
bj-ax12i 30803 and label suggestions are welcome for the
others. I also
propose to change to
in speimfw 1761 and spimfw 1763
(other spim* theorems use and
very very few theorems in set.mm
use ). (Contributed by BJ,
29-Sep-2019.) |