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	$$⊢\mathrm{E}\mathrm{Fr}A\to \forall x\in A\neg x\in x$$

Proof

Step	Hyp	Ref	Expression
1		frirr	$$⊢\left(\mathrm{E}\mathrm{Fr}A\wedge x\in A\right)\to \neg x\mathrm{E}x$$
2		epel	$$⊢x\mathrm{E}x\leftrightarrow x\in x$$
3	1 2	sylnib	$$⊢\left(\mathrm{E}\mathrm{Fr}A\wedge x\in A\right)\to \neg x\in x$$
4	3	ralrimiva	$$⊢\mathrm{E}\mathrm{Fr}A\to \forall x\in A\neg x\in x$$