Metamath Proof Explorer

Theorem efrn2lp

Description: A well-founded class contains no 2-cycle loops. (Contributed by NM, 19-Apr-1994)

Ref Expression
Assertion efrn2lp ⊢EFrA∧B∈A∧C∈A→¬B∈C∧C∈B

Proof

Step Hyp Ref Expression
1 fr2nr ⊢EFrA∧B∈A∧C∈A→¬BEC∧CEB
2 epelg ⊢C∈A→BEC↔B∈C
3 epelg ⊢B∈A→CEB↔C∈B
4 2 3 bi2anan9r ⊢B∈A∧C∈A→BEC∧CEB↔B∈C∧C∈B
5 4 adantl ⊢EFrA∧B∈A∧C∈A→BEC∧CEB↔B∈C∧C∈B
6 1 5 mtbid ⊢EFrA∧B∈A∧C∈A→¬B∈C∧C∈B