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 ∈ V ∧ B ∈ W ∧ C ∈ X → A Redunds B C ↔ A Redund B C

Proof

Step Hyp Ref Expression
1 brredunds ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → A Redunds B C ↔ A ⊆ B ∧ A ∩ C = B ∩ C
2 df-redund ⊢ A Redund B C ↔ A ⊆ B ∧ A ∩ C = B ∩ C
3 1 2 bitr4di ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → A Redunds B C ↔ A Redund B C