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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 Redunds ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 Redund ⟨ 𝐵 , 𝐶 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		brredunds	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 Redunds ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) ) )
2		df-redund	⊢ ( 𝐴 Redund ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) )
3	1 2	bitr4di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 Redunds ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 Redund ⟨ 𝐵 , 𝐶 ⟩ ) )