# Metamath Proof Explorer

## Theorem aev2

Description: 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 -> , <-> , /\ , \/ , T. , = , A. , E. , E* , E! , F/ . An example is given by aevdemo . This list cannot be extended to -. or F. since the scheme A. x x = y is consistent with ax-mp , ax-gen , ax-1 -- ax-13 (as the one-element universe shows).

(Contributed by BJ, 23-Mar-2021)

Ref Expression
Assertion aev2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}\forall {t}\phantom{\rule{.4em}{0ex}}{u}={v}$

### Proof

Step Hyp Ref Expression
1 aev ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {w}\phantom{\rule{.4em}{0ex}}{w}={s}$
2 aev ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}{w}={s}\to \forall {t}\phantom{\rule{.4em}{0ex}}{u}={v}$
3 2 alrimiv ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}{w}={s}\to \forall {z}\phantom{\rule{.4em}{0ex}}\forall {t}\phantom{\rule{.4em}{0ex}}{u}={v}$
4 1 3 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}\forall {t}\phantom{\rule{.4em}{0ex}}{u}={v}$