Theorem eleccnvep

Description: Elementhood in the converse epsilon coset of A is elementhood in A . (Contributed by Peter Mazsa, 27-Jan-2019)

	Ref	Expression
Assertion	eleccnvep	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ∈ [ 𝐴 ] ◡ E ↔ 𝐵 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ E
2		relelec	⊢ ( Rel ◡ E → ( 𝐵 ∈ [ 𝐴 ] ◡ E ↔ 𝐴 ◡ E 𝐵 ) )
3	1 2	ax-mp	⊢ ( 𝐵 ∈ [ 𝐴 ] ◡ E ↔ 𝐴 ◡ E 𝐵 )
4		brcnvep	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ◡ E 𝐵 ↔ 𝐵 ∈ 𝐴 ) )
5	3 4	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ∈ [ 𝐴 ] ◡ E ↔ 𝐵 ∈ 𝐴 ) )