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	|- ( M |=. Ax-Ext <-> A. x e. M A. y e. M ( A. z e. M ( z e. x <-> z e. y ) -> x = y ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cM	|- M
1	0	wsmext	|- M |=. Ax-Ext
2		vx	|- x
3		vy	|- y
4		vz	|- z
5	4	cv	|- z
6	2	cv	|- x
7	5 6	wcel	|- z e. x
8	3	cv	|- y
9	5 8	wcel	|- z e. y
10	7 9	wb	|- ( z e. x <-> z e. y )
11	10 4 0	wral	|- A. z e. M ( z e. x <-> z e. y )
12	6 8	wceq	|- x = y
13	11 12	wi	|- ( A. z e. M ( z e. x <-> z e. y ) -> x = y )
14	13 3 0	wral	|- A. y e. M ( A. z e. M ( z e. x <-> z e. y ) -> x = y )
15	14 2 0	wral	|- A. x e. M A. y e. M ( A. z e. M ( z e. x <-> z e. y ) -> x = y )
16	1 15	wb	|- ( M |=. Ax-Ext <-> A. x e. M A. y e. M ( A. z e. M ( z e. x <-> z e. y ) -> x = y ) )