Theorem hbaev

All variables are effectively bound in an identical variable specifier. Version of hbae with a disjoint variable condition, requiring fewer axioms. Instance of aev2. (Contributed by NM, 13-May-1993.) Reduce axiom usage. (Revised by Wolf Lammen, 22-Mar-2021.)

Conclusion

\( \vdash \forall x \, x = y' \rightarrow \forall z \, \forall x \, x = y' \)

Proof

aev2

\( \vdash \forall x \, x = y' \rightarrow \forall z \, \forall w \, w = y' \)

cbvaev

\( \vdash \forall w \, w = y' \rightarrow \forall x \, x = y' \)

alimi _

syl l0 _