Metamath Proof Explorer

Theorem elpredg

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011)

Ref Expression
Assertion elpredg ⊢ X ∈ B ∧ Y ∈ A → Y ∈ Pred R A X ↔ Y R X

Proof

Step Hyp Ref Expression
1 df-pred ⊢ Pred R A X = A ∩ R -1 X
2 1 elin2 ⊢ Y ∈ Pred R A X ↔ Y ∈ A ∧ Y ∈ R -1 X
3 2 baib ⊢ Y ∈ A → Y ∈ Pred R A X ↔ Y ∈ R -1 X
4 3 adantl ⊢ X ∈ B ∧ Y ∈ A → Y ∈ Pred R A X ↔ Y ∈ R -1 X
5 elimasng ⊢ X ∈ B ∧ Y ∈ A → Y ∈ R -1 X ↔ X Y ∈ R -1
6 df-br ⊢ X R -1 Y ↔ X Y ∈ R -1
7 5 6 syl6bbr ⊢ X ∈ B ∧ Y ∈ A → Y ∈ R -1 X ↔ X R -1 Y
8 brcnvg ⊢ X ∈ B ∧ Y ∈ A → X R -1 Y ↔ Y R X
9 4 7 8 3bitrd ⊢ X ∈ B ∧ Y ∈ A → Y ∈ Pred R A X ↔ Y R X