Metamath Proof Explorer

Theorem brredundsredund

Description: For sets, binary relation on the class of all redundant sets ( brredunds ) is equivalent to satisfying the redundancy predicate ( df-redund ). (Contributed by Peter Mazsa, 25-Oct-2022)

		Ref	Expression
	Assertion	brredundsredund	$⊢ (A \in V \land B \in W \land C \in X) \to (A Redunds ⟨B, C⟩ \leftrightarrow A Redund ⟨B, C⟩)$

Proof

Step	Hyp	Ref	Expression
1		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))$
2		df-redund	$⊢ A Redund ⟨B, C⟩ \leftrightarrow (A \subseteq B \land A \cap C = B \cap C)$
3	1 2	bitr4di	$⊢ (A \in V \land B \in W \land C \in X) \to (A Redunds ⟨B, C⟩ \leftrightarrow A Redund ⟨B, C⟩)$