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 -> A. x e. A -. x e. x )

Proof

Step Hyp Ref Expression
1 frirr 
 |-  ( ( _E Fr A /\ x e. A ) -> -. x _E x )
2 epel 
 |-  ( x _E x <-> x e. x )
3 1 2 sylnib 
 |-  ( ( _E Fr A /\ x e. A ) -> -. x e. x )
4 3 ralrimiva 
 |-  ( _E Fr A -> A. x e. A -. x e. x )