On the official website there is the wff theorem weq which is proved from the syntax definition wceq.
However the corresponding metamath-web page shows weq as a derivable statement https://metamath.tirix.org/mpests/weq, which does not match the official website and it is also not true in general.
EDIT: also the metamath-web page does not show its proof.
On the official website there is the wff theorem weq which is proved from the syntax definition wceq.
However the corresponding metamath-web page shows
weqas a derivable statement https://metamath.tirix.org/mpests/weq, which does not match the official website and it is also not true in general.EDIT: also the metamath-web page does not show its proof.