Definition df-smext

Description: Define the standard model of Extensionality predicate, which is true for a class that is a model of the Axiom of Extensionality under the membership predicate. Our notation is similar to that of df-prv and df-gzext ( M |= AxExt ), but M |=. Ax-Ext uses a different double turnstile character and a different format for the axiom name. (Contributed by BTernaryTau, 2-Oct-2026)

	Ref	Expression
Assertion	df-smext	Could not format assertion : No typesetting found for |- ( M |=. Ax-Ext <-> A. x e. M A. y e. M ( A. z e. M ( z e. x <-> z e. y ) -> x = y ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cM	$$classM$$
1	0	wsmext	Could not format M |=. Ax-Ext : No typesetting found for wff M |=. Ax-Ext with typecode wff
2		vx	$$setvarx$$
3		vy	$$setvary$$
4		vz	$$setvarz$$
5	4	cv	$$setvarz$$
6	2	cv	$$setvarx$$
7	5 6	wcel	$$wffz\in x$$
8	3	cv	$$setvary$$
9	5 8	wcel	$$wffz\in y$$
10	7 9	wb	$$wff\left(z\in x\leftrightarrow z\in y\right)$$
11	10 4 0	wral	$$wff\forall z\in M\left(z\in x\leftrightarrow z\in y\right)$$
12	6 8	wceq	$$wffx=y$$
13	11 12	wi	$$wff\left(\forall z\in M\left(z\in x\leftrightarrow z\in y\right)\to x=y\right)$$
14	13 3 0	wral	$$wff\forall y\in M\left(\forall z\in M\left(z\in x\leftrightarrow z\in y\right)\to x=y\right)$$
15	14 2 0	wral	$$wff\forall x\in M\forall y\in M\left(\forall z\in M\left(z\in x\leftrightarrow z\in y\right)\to x=y\right)$$
16	1 15	wb	Could not format ( M |=. Ax-Ext <-> A. x e. M A. y e. M ( A. z e. M ( z e. x <-> z e. y ) -> x = y ) ) : No typesetting found for wff ( M |=. Ax-Ext <-> A. x e. M A. y e. M ( A. z e. M ( z e. x <-> z e. y ) -> x = y ) ) with typecode wff