Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-redund Structured version   Visualization version   GIF version

Definition df-redund 36724
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.)
Assertion
Ref Expression
df-redund (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴𝐵 ∧ (𝐴𝐶) = (𝐵𝐶)))

Detailed syntax breakdown of Definition df-redund
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cC . . 3 class 𝐶
41, 2, 3wredund 36341 . 2 wff 𝐴 Redund ⟨𝐵, 𝐶
51, 2wss 3888 . . 3 wff 𝐴𝐵
61, 3cin 3887 . . . 4 class (𝐴𝐶)
72, 3cin 3887 . . . 4 class (𝐵𝐶)
86, 7wceq 1539 . . 3 wff (𝐴𝐶) = (𝐵𝐶)
95, 8wa 396 . 2 wff (𝐴𝐵 ∧ (𝐴𝐶) = (𝐵𝐶))
104, 9wb 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