Theorem axc9

Derive set.mm's original [ax-c9] from the shorter [ax-13]. Usage is discouraged to avoid uninformed [ax-13] propagation. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Proof shortened by Wolf Lammen, 29-Apr-2018.) (New usage is discouraged.)

Conclusion
\( \vdash \neg \forall z \, z = x' \rightarrow \neg \forall z \, z = y' \rightarrow x' = y' \rightarrow \forall z \, x' = y' \)
Proof
nfeqf
nf5rd _
ex _