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

Metamath Proof Explorer

Theorem efrunt

Description: If A is well-founded by _E , then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011)

		Ref	Expression
	Assertion	efrunt	$⊢ E Fr A \to \forall x \in A \neg x \in x$

Step	Hyp	Ref	Expression
1		frirr	$⊢ (E Fr A \land x \in A) \to \neg x E x$
2		epel	$⊢ x E x \leftrightarrow x \in x$
3	1 2	sylnib	$⊢ (E Fr A \land x \in A) \to \neg x \in x$
4	3	ralrimiva	$⊢ E Fr A \to \forall x \in A \neg x \in x$