Mathbox for Emmett Weisz < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-setrecs Structured version   Visualization version   GIF version

Definition df-setrecs 44094
Assertion
Ref Expression
df-setrecs setrecs(𝐹) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
Distinct variable group:   𝑦,𝑧,𝑤,𝐹

Detailed syntax breakdown of Definition df-setrecs
StepHypRef Expression
1 cF . . 3 class 𝐹
21csetrecs 44093 . 2 class setrecs(𝐹)
3 vw . . . . . . . . . 10 setvar 𝑤
43cv 1506 . . . . . . . . 9 class 𝑤
5 vy . . . . . . . . . 10 setvar 𝑦
65cv 1506 . . . . . . . . 9 class 𝑦
74, 6wss 3825 . . . . . . . 8 wff 𝑤𝑦
8 vz . . . . . . . . . . 11 setvar 𝑧
98cv 1506 . . . . . . . . . 10 class 𝑧
104, 9wss 3825 . . . . . . . . 9 wff 𝑤𝑧
114, 1cfv 6182 . . . . . . . . . 10 class (𝐹𝑤)
1211, 9wss 3825 . . . . . . . . 9 wff (𝐹𝑤) ⊆ 𝑧
1310, 12wi 4 . . . . . . . 8 wff (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)
147, 13wi 4 . . . . . . 7 wff (𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧))
1514, 3wal 1505 . . . . . 6 wff 𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧))
166, 9wss 3825 . . . . . 6 wff 𝑦𝑧
1715, 16wi 4 . . . . 5 wff (∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)
1817, 8wal 1505 . . . 4 wff 𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)
1918, 5cab 2753 . . 3 class {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
2019cuni 4706 . 2 class {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
212, 20wceq 1507 1 wff setrecs(𝐹) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
 Colors of variables: wff setvar class This definition is referenced by:  setrecseq  44095  nfsetrecs  44096  setrec1  44101  setrec2fun  44102  setrec2  44105
 Copyright terms: Public domain W3C validator