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 35991
 Description: Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 35993) 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 35606 . 2 wff 𝐴 Redund ⟨𝐵, 𝐶
51, 2wss 3919 . . 3 wff 𝐴𝐵
61, 3cin 3918 . . . 4 class (𝐴𝐶)
72, 3cin 3918 . . . 4 class (𝐵𝐶)
86, 7wceq 1538 . . 3 wff (𝐴𝐶) = (𝐵𝐶)
95, 8wa 399 . 2 wff (𝐴𝐵 ∧ (𝐴𝐶) = (𝐵𝐶))
104, 9wb 209 1 wff (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴𝐵 ∧ (𝐴𝐶) = (𝐵𝐶)))
 Colors of variables: wff setvar class This definition is referenced by:  brredundsredund  35994  redundss3  35995  redundeq1  35996  refrelsredund4  35999
 Copyright terms: Public domain W3C validator