Theorem aev2

A version of aev with two universal quantifiers in the consequent. One can prove similar statements with arbitrary numbers of universal quantifiers in the consequent (the series begins with aeveq, aev, aev2 ).

Using aev and alrimiv, one can actually prove (with no more axioms) any scheme of the form ( A. x x = y -> PHI) , DV ( x , y ) where PHI involves only setvar variables and the connectors ->, <->, /\, \/, \( \top \), =, A., E., E*, E!, F/. An example is given by [aevdemo]. This list cannot be extended to -. or \( \bot \) since the scheme \( \forall x \, x = y' \) is consistent with [ax-mp], [ax-gen], [ax-1] -- [ax-13] (as the one-element universe shows), so for instance ( A. x x = y -> F. ) , DV ( x , y ) is not provable from these axioms alone (indeed, [dtru] uses non-logical axioms as well). (Contributed by BJ, 23-Mar-2021.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \forall z \, \forall t \, u' = v' \)
Proof
l0
aev
\( \vdash \forall x \, x = y' \rightarrow \forall w \, w = s \)
aev
alrimiv _
\( \vdash \forall w \, w = s \rightarrow \forall z \, \forall t \, u' = v' \)
syl l0 _