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

Metamath Proof Explorer

Theorem extep

Description: Property of epsilon relation, see also extid , extssr and the comment of df-ssr . (Contributed by Peter Mazsa, 10-Jul-2019)

		Ref	Expression
	Assertion	extep	$⊢ (A \in V \land B \in W) \to ([A] E^{-1} = [B] E^{-1} \leftrightarrow A = B)$

Step	Hyp	Ref	Expression
1		eccnvep	$⊢ A \in V \to [A] E^{-1} = A$
2		eccnvep	$⊢ B \in W \to [B] E^{-1} = B$
3	1 2	eqeqan12d	$⊢ (A \in V \land B \in W) \to ([A] E^{-1} = [B] E^{-1} \leftrightarrow A = B)$