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	⊢ ( 𝑀 ⊨ Ax-Ext ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cM	⊢ 𝑀
1	0	wsmext	⊢ 𝑀 ⊨ Ax-Ext
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4		vz	⊢ 𝑧
5	4	cv	⊢ 𝑧
6	2	cv	⊢ 𝑥
7	5 6	wcel	⊢ 𝑧 ∈ 𝑥
8	3	cv	⊢ 𝑦
9	5 8	wcel	⊢ 𝑧 ∈ 𝑦
10	7 9	wb	⊢ ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 )
11	10 4 0	wral	⊢ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 )
12	6 8	wceq	⊢ 𝑥 = 𝑦
13	11 12	wi	⊢ ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )
14	13 3 0	wral	⊢ ∀ 𝑦 ∈ 𝑀 ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )
15	14 2 0	wral	⊢ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )
16	1 15	wb	⊢ ( 𝑀 ⊨ Ax-Ext ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )