Metamath Proof Explorer

Theorem relelec

Description: Membership in an equivalence class when R is a relation. (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Assertion relelec ⊢ Rel ⁡ R → A ∈ B R ↔ B R A

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ B R → A ∈ V
2 ecexr ⊢ A ∈ B R → B ∈ V
3 1 2 jca ⊢ A ∈ B R → A ∈ V ∧ B ∈ V
4 3 adantl ⊢ Rel ⁡ R ∧ A ∈ B R → A ∈ V ∧ B ∈ V
5 brrelex12 ⊢ Rel ⁡ R ∧ B R A → B ∈ V ∧ A ∈ V
6 5 ancomd ⊢ Rel ⁡ R ∧ B R A → A ∈ V ∧ B ∈ V
7 elecg ⊢ A ∈ V ∧ B ∈ V → A ∈ B R ↔ B R A
8 4 6 7 pm5.21nd ⊢ Rel ⁡ R → A ∈ B R ↔ B R A