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

Metamath Proof Explorer

Theorem ruALT

Description: Alternate proof of ru , simplified using (indirectly) the Axiom of Regularity ax-reg . (Contributed by Alan Sare, 4-Oct-2008) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ruALT	⊢ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∉ V

Proof

Step	Hyp	Ref	Expression
1		vprc	⊢ ¬ V ∈ V
2	1	nelir	⊢ V ∉ V
3		ruv	⊢ { 𝑥 ∣ 𝑥 ∉ 𝑥 } = V
4		neleq1	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } = V → ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∉ V ↔ V ∉ V ) )
5	3 4	ax-mp	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∉ V ↔ V ∉ V )
6	2 5	mpbir	⊢ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∉ V