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 ⊢ E Fr A ∧ B ∈ A ∧ C ∈ A → ¬ B ∈ C ∧ C ∈ B

Proof

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