Metamath Proof Explorer


Syntax definition wsmext

Description: Extend wff notation to include a predicate for standard models of the Axiom of Extensionality.

Ref Expression
Assertion wsmext wff 𝑀 ⊨ Ax-Ext