Theorem traxext

Description: A transitive class models the Axiom of Extensionality ax-ext . Lemma II.2.4(1) of Kunen2 p. 111. (Contributed by Eric Schmidt, 11-Sep-2025)

	Ref	Expression
Assertion	traxext	⊢ ( Tr 𝑀 → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
2		trel	⊢ ( Tr 𝑀 → ( ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑀 ) → 𝑧 ∈ 𝑀 ) )
3	2	ancomsd	⊢ ( Tr 𝑀 → ( ( 𝑥 ∈ 𝑀 ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑀 ) )
4	3	expdimp	⊢ ( ( Tr 𝑀 ∧ 𝑥 ∈ 𝑀 ) → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑀 ) )
5	4	adantrr	⊢ ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑀 ) )
6	5	adantr	⊢ ( ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ) → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑀 ) )
7		trel	⊢ ( Tr 𝑀 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑀 ) → 𝑧 ∈ 𝑀 ) )
8	7	ancomsd	⊢ ( Tr 𝑀 → ( ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑀 ) )
9	8	expdimp	⊢ ( ( Tr 𝑀 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑀 ) )
10	9	adantrl	⊢ ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑀 ) )
11	10	adantr	⊢ ( ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ) → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑀 ) )
12		simpr	⊢ ( ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ) → ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
13	6 11 12	pm5.21ndd	⊢ ( ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ) → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )
14	13	ex	⊢ ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) → ( ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
15	14	alimdv	⊢ ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
16	1 15	biimtrid	⊢ ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) → ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
17		ax-ext	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )
18	16 17	syl6	⊢ ( ( Tr 𝑀 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) → ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
19	18	ralrimivva	⊢ ( Tr 𝑀 → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )