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

Definition df-redunds 36391
Description: Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 36394) is equivalent to satisfying the redundancy predicate (df-redund 36392). (Contributed by Peter Mazsa, 23-Oct-2022.)
Assertion
Ref Expression
df-redunds Redunds = {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥𝑦 ∧ (𝑥𝑧) = (𝑦𝑧))}
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-redunds
StepHypRef Expression
1 credunds 36008 . 2 class Redunds
2 vx . . . . . . 7 setvar 𝑥
32cv 1541 . . . . . 6 class 𝑥
4 vy . . . . . . 7 setvar 𝑦
54cv 1541 . . . . . 6 class 𝑦
63, 5wss 3853 . . . . 5 wff 𝑥𝑦
7 vz . . . . . . . 8 setvar 𝑧
87cv 1541 . . . . . . 7 class 𝑧
93, 8cin 3852 . . . . . 6 class (𝑥𝑧)
105, 8cin 3852 . . . . . 6 class (𝑦𝑧)
119, 10wceq 1542 . . . . 5 wff (𝑥𝑧) = (𝑦𝑧)
126, 11wa 399 . . . 4 wff (𝑥𝑦 ∧ (𝑥𝑧) = (𝑦𝑧))
1312, 4, 7, 2coprab 7183 . . 3 class {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥𝑦 ∧ (𝑥𝑧) = (𝑦𝑧))}
1413ccnv 5534 . 2 class {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥𝑦 ∧ (𝑥𝑧) = (𝑦𝑧))}
151, 14wceq 1542 1 wff Redunds = {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥𝑦 ∧ (𝑥𝑧) = (𝑦𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  brredunds  36394
  Copyright terms: Public domain W3C validator