Definition df-smext 36002

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 36197 and df-gzext 36304 (𝑀⊧AxExt), but 𝑀 ⊨ Ax-Ext uses a different double turnstile character and a different format for the axiom name. (Contributed by BTernaryTau, 2-Oct-2026.)

Assertion

Ref	Expression
df-smext	⊢ (𝑀 ⊨ Ax-Ext ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))

Distinct variable group:   𝑥,𝑀,𝑦,𝑧

Detailed syntax breakdown of Definition df-smext

Step	Hyp	Ref	Expression
1		cM	. . 3 class 𝑀
2	1	wsmext 36000	. 2 wff 𝑀 ⊨ Ax-Ext
3		vz	. . . . . . . 8 setvar 𝑧
4		vx	. . . . . . . 8 setvar 𝑥
5	3, 4	wel 2145	. . . . . . 7 wff 𝑧 ∈ 𝑥
6		vy	. . . . . . . 8 setvar 𝑦
7	3, 6	wel 2145	. . . . . . 7 wff 𝑧 ∈ 𝑦
8	5, 7	wb 209	. . . . . 6 wff (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)
9	8, 3, 1	wral 3076	. . . . 5 wff ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)
10	4, 6	weq 1994	. . . . 5 wff 𝑥 = 𝑦
11	9, 10	wi 4	. . . 4 wff (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
12	11, 6, 1	wral 3076	. . 3 wff ∀𝑦 ∈ 𝑀 (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
13	12, 4, 1	wral 3076	. 2 wff ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
14	2, 13	wb 209	1 wff (𝑀 ⊨ Ax-Ext ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))

This definition is used by:  vsmext  36008