This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brcnvep

Description: The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018)

Ref Expression
Assertion brcnvep ⊢ A ∈ V → A E -1 B ↔ B ∈ A

Proof

Step Hyp Ref Expression
1 rele ⊢ Rel ⁡ E
2 1 relbrcnv ⊢ A E -1 B ↔ B E A
3 epelg ⊢ A ∈ V → B E A ↔ B ∈ A
4 2 3 bitrid ⊢ A ∈ V → A E -1 B ↔ B ∈ A