Metamath Proof Explorer

Theorem elrelimasn

Description: Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015)

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

Proof

Step Hyp Ref Expression
1 relimasn ⊢ Rel ⁡ R → R A = x | A R x
2 1 eleq2d ⊢ Rel ⁡ R → B ∈ R A ↔ B ∈ x | A R x
3 brrelex2 ⊢ Rel ⁡ R ∧ A R B → B ∈ V
4 3 ex ⊢ Rel ⁡ R → A R B → B ∈ V
5 breq2 ⊢ x = B → A R x ↔ A R B
6 5 elab3g ⊢ A R B → B ∈ V → B ∈ x | A R x ↔ A R B
7 4 6 syl ⊢ Rel ⁡ R → B ∈ x | A R x ↔ A R B
8 2 7 bitrd ⊢ Rel ⁡ R → B ∈ R A ↔ A R B