Theorem brcnvep

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

	Ref	Expression
Assertion	brcnvep	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ◡ E 𝐵 ↔ 𝐵 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rele	⊢ Rel E
2	1	relbrcnv	⊢ ( 𝐴 ◡ E 𝐵 ↔ 𝐵 E 𝐴 )
3		epelg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 E 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
4	2 3	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ◡ E 𝐵 ↔ 𝐵 ∈ 𝐴 ) )