Entry Value
Package Name set-def
Count 22
Theorems
  • BIJ : !s t. BIJ s t = INJ s t INTER SURJ s t
  • CHOICE : !s. ~(s = {}) ==> CHOICE s IN s
  • CROSS : !s t. s CROSS t = {x,y | x IN s /\ y IN t}
  • DELETE : !s x. s DELETE x = {y | y IN s /\ ~(y = x)}
  • DIFF : !s t. s DIFF t = {x | x IN s /\ ~(x IN t)}
  • DISJOINT : !s t. DISJOINT s t <=> s INTER t = {}
  • EMPTY : {} = {x | F}
  • EXTENSION_IMP : !s t. (!x. x IN s <=> x IN t) ==> s = t
  • IMAGE : !f s. IMAGE f s = {y | ?x. x IN s /\ y = f x}
  • INJ : !s t. INJ s t = {f | (!x. x IN s ==> f x IN t) /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)}
  • INSERT : !x s. x INSERT s = {y | y = x \/ y IN s}
  • INTER : !s t. s INTER t = {x | x IN s /\ x IN t}
  • INTERS : !s. INTERS s = {x | !u. u IN s ==> x IN u}
  • IN_ELIM_THM : !p x. x IN GSPEC p <=> p x
  • PSUBSET : !s t. s PSUBSET t <=> s SUBSET t /\ ~(s = t)
  • REST : !s. REST s = s DELETE CHOICE s
  • SING : !s. SING s <=> (?x. s = {x})
  • SUBSET : !s t. s SUBSET t <=> (!x. x IN s ==> x IN t)
  • SURJ : !s t. SURJ s t = {f | (!x. x IN s ==> f x IN t) /\ (!x. x IN t ==> (?y. y IN s /\ f y = x))}
  • UNION : !s t. s UNION t = {x | x IN s \/ x IN t}
  • UNIONS : !s. UNIONS s = {x | ?u. u IN s /\ x IN u}
  • UNIV : UNIV = {x | T}
  • Back to main package page