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

Metamath Proof Explorer

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	$⊢ A \in V \to (B \in [A] E^{-1} \leftrightarrow B \in A)$

Step	Hyp	Ref	Expression
1		relcnv	$⊢ Rel E^{-1}$
2		relelec	$⊢ Rel E^{-1} \to (B \in [A] E^{-1} \leftrightarrow A E^{-1} B)$
3	1 2	ax-mp	$⊢ B \in [A] E^{-1} \leftrightarrow A E^{-1} B$
4		brcnvep	$⊢ A \in V \to (A E^{-1} B \leftrightarrow B \in A)$
5	3 4	bitrid	$⊢ A \in V \to (B \in [A] E^{-1} \leftrightarrow B \in A)$