brredunds

Description: Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022)

		Ref	Expression
	Assertion	brredunds	$⊢ (A \in V \land B \in W \land C \in X) \to (A Redunds ⟨B, C⟩ \leftrightarrow (A \subseteq B \land A \cap C = B \cap C))$

Step	Hyp	Ref	Expression
1		sseq12	$⊢ (x = A \land y = B) \to (x \subseteq y \leftrightarrow A \subseteq B)$
2	1	3adant3	$⊢ (x = A \land y = B \land z = C) \to (x \subseteq y \leftrightarrow A \subseteq B)$
3		ineq12	$⊢ (x = A \land z = C) \to x \cap z = A \cap C$
4	3	3adant2	$⊢ (x = A \land y = B \land z = C) \to x \cap z = A \cap C$
5		ineq12	$⊢ (y = B \land z = C) \to y \cap z = B \cap C$
6	5	3adant1	$⊢ (x = A \land y = B \land z = C) \to y \cap z = B \cap C$
7	4 6	eqeq12d	$⊢ (x = A \land y = B \land z = C) \to (x \cap z = y \cap z \leftrightarrow A \cap C = B \cap C)$
8	2 7	anbi12d	$⊢ (x = A \land y = B \land z = C) \to ((x \subseteq y \land x \cap z = y \cap z) \leftrightarrow (A \subseteq B \land A \cap C = B \cap C))$
9		df-redunds	$⊢ Redunds = {\{⟨⟨y, z⟩, x⟩ \| (x \subseteq y \land x \cap z = y \cap z)\}}^{-1}$
10	8 9	brcnvrabga	$⊢ (A \in V \land B \in W \land C \in X) \to (A Redunds ⟨B, C⟩ \leftrightarrow (A \subseteq B \land A \cap C = B \cap C))$

Metamath Proof Explorer