Description: An ordinal number is not a member of itself. Theorem 7M(c) of Enderton p. 192. (Contributed by NM, 11-Jun-1994)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | on.1 | ⊢ 𝐴 ∈ On | |
| Assertion | onirri | ⊢ ¬ 𝐴 ∈ 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | on.1 | ⊢ 𝐴 ∈ On | |
| 2 | 1 | onordi | ⊢ Ord 𝐴 |
| 3 | ordirr | ⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 ) | |
| 4 | 2 3 | ax-mp | ⊢ ¬ 𝐴 ∈ 𝐴 |