Theorem cbvaev

Change bound variable in an equality with a disjoint variable condition. Instance of aev. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \forall z \, z = y' \)
Proof
ax7
l1
cbvalivw _
\( \vdash \forall x \, x = y' \rightarrow \forall t \, t = y' \)
ax7
cbvalivw _
\( \vdash \forall t \, t = y' \rightarrow \forall z \, z = y' \)
syl l1 _