Definition df-redunds

Description: Define the class of all redundant sets x with respect to y in z . 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, 23-Oct-2022)

	Ref	Expression
Assertion	df-redunds	⊢ Redunds = ◡ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑧 ) = ( 𝑦 ∩ 𝑧 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		credunds	⊢ Redunds
1		vy	⊢ 𝑦
2		vz	⊢ 𝑧
3		vx	⊢ 𝑥
4	3	cv	⊢ 𝑥
5	1	cv	⊢ 𝑦
6	4 5	wss	⊢ 𝑥 ⊆ 𝑦
7	2	cv	⊢ 𝑧
8	4 7	cin	⊢ ( 𝑥 ∩ 𝑧 )
9	5 7	cin	⊢ ( 𝑦 ∩ 𝑧 )
10	8 9	wceq	⊢ ( 𝑥 ∩ 𝑧 ) = ( 𝑦 ∩ 𝑧 )
11	6 10	wa	⊢ ( 𝑥 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑧 ) = ( 𝑦 ∩ 𝑧 ) )
12	11 1 2 3	coprab	⊢ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑧 ) = ( 𝑦 ∩ 𝑧 ) ) }
13	12	ccnv	⊢ ◡ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑧 ) = ( 𝑦 ∩ 𝑧 ) ) }
14	0 13	wceq	⊢ Redunds = ◡ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑧 ) = ( 𝑦 ∩ 𝑧 ) ) }