Metamath Proof Explorer

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 ⁡ M → ∀ x ∈ M ∀ y ∈ M ∀ z ∈ M z ∈ x ↔ z ∈ y → x = y

Proof

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