Description: A version of aev 1983
with two universal quantifiers in the consequent, and
a generalization of hbaevg 1984. One can prove similar statements with
arbitrary numbers of universal quantifiers in the consequent (the series
begins with aeveq 1982, aev 1983, aev2 1986).
Using aev 1983 and alrimiv 1855 (as in aev2ALT 1987), one can actually prove
(with no more axioms) any scheme of the form
PHI) ,
DV where PHI
involves only setvar variables and the
connectors , , , ,
, ,
, , , , . An example is given by
aevdemo 27317. This list cannot be extended to or since the
scheme is consistent with ax-mp 5, ax-gen 1722, ax-1 6--
ax-13 2246 (as the one-element universe shows).
(Contributed by BJ, 29-Mar-2021.) |