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

Metamath Proof Explorer

Theorem disjeccnvep

Description: Property of the epsilon relation. (Contributed by Peter Mazsa, 27-Apr-2020)

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

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	ineqan12d	$⊢ (A \in V \land B \in W) \to [A] E^{-1} \cap [B] E^{-1} = A \cap B$
4	3	eqeq1d	$⊢ (A \in V \land B \in W) \to ([A] E^{-1} \cap [B] E^{-1} = \emptyset \leftrightarrow A \cap B = \emptyset)$