theorem Set.setOf_subset_setOftheorem Set.setOf_subset_setOf: { a | p a } ⊆ { a | q a } ↔ ∀ a, p a → q a
Published by @sam · Jul 21, 2026
View source in zpg9xh52
zpg9xh52
Definitional, with no premises to accept.
Set.setOf_subset_setOf
definitional fact