Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-redund | Structured version Visualization version GIF version |
Description: Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 36726) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.) |
Ref | Expression |
---|---|
df-redund | ⊢ (𝐴 Redund 〈𝐵, 𝐶〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cC | . . 3 class 𝐶 | |
4 | 1, 2, 3 | wredund 36341 | . 2 wff 𝐴 Redund 〈𝐵, 𝐶〉 |
5 | 1, 2 | wss 3888 | . . 3 wff 𝐴 ⊆ 𝐵 |
6 | 1, 3 | cin 3887 | . . . 4 class (𝐴 ∩ 𝐶) |
7 | 2, 3 | cin 3887 | . . . 4 class (𝐵 ∩ 𝐶) |
8 | 6, 7 | wceq 1539 | . . 3 wff (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) |
9 | 5, 8 | wa 396 | . 2 wff (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
10 | 4, 9 | wb 205 | 1 wff (𝐴 Redund 〈𝐵, 𝐶〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))) |
Colors of variables: wff setvar class |
This definition is referenced by: brredundsredund 36727 redundss3 36728 redundeq1 36729 refrelsredund4 36732 |
Copyright terms: Public domain | W3C validator |