This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem untelirr

Description: We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 ). Using this concept, we can avoid a lot of the uses of the Axiom of Regularity. Here, we prove a series of properties of untanged classes. First, we prove that an untangled class is not a member of itself. (Contributed by Scott Fenton, 28-Feb-2011)

Ref Expression
Assertion untelirr ⊢ ∀ x ∈ A ¬ x ∈ x → ¬ A ∈ A

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ x = A → x ∈ x ↔ A ∈ x
2 eleq2 ⊢ x = A → A ∈ x ↔ A ∈ A
3 1 2 bitrd ⊢ x = A → x ∈ x ↔ A ∈ A
4 3 notbid ⊢ x = A → ¬ x ∈ x ↔ ¬ A ∈ A
5 4 rspccv ⊢ ∀ x ∈ A ¬ x ∈ x → A ∈ A → ¬ A ∈ A
6 5 pm2.01d ⊢ ∀ x ∈ A ¬ x ∈ x → ¬ A ∈ A