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	$⊢ \{x \| x \notin x\} \notin V$

Proof

Step	Hyp	Ref	Expression
1		vprc	$⊢ \neg V \in V$
2	1	nelir	$⊢ V \notin V$
3		ruv	$⊢ \{x \| x \notin x\} = V$
4		neleq1	$⊢ \{x \| x \notin x\} = V \to (\{x \| x \notin x\} \notin V \leftrightarrow V \notin V)$
5	3 4	ax-mp	$⊢ \{x \| x \notin x\} \notin V \leftrightarrow V \notin V$
6	2 5	mpbir	$⊢ \{x \| x \notin x\} \notin V$