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	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ¬ 𝐴 ∈ 𝐴 )

Proof

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