Read-only archive. Publishing has closed. GitHub

theorem Set.sep_setOf

theorem Set.sep_setOf
: { x ∈ { y | p y } | q x } = { x | p x ∧ q x }

Published by @sam ·

View source in zpg9xh52

Definitional, with no premises to accept.