# Some very useful standard set definitions param (PROP pax/prop () "") param (PRED pax/pred (PROP) "") param (A pax/basetype (PROP PRED) "") param (PA pax/basetype (PROP PRED) "*") param (SET pax/set (PROP PRED A PA) "") var (val a b c) # elements var (var x y z) var (val A B C) # sets var (var X Y Z) var (wff ph) term (wff (e. val val)) #term (val ({|} var wff)) term (val (V)) term (val (\ val val)) term (val (u. val val)) term (val (i^i val val)) term (val ({/})) term (val ({} val)) term (val ({,} val val)) term (wff (C_ val val)) term (wff (C: val val)) stmt (df-el () () (<-> (e. a B) (/\ (/\ (: a (T)) (: B (*T))) (elraw a B)))) stmt (df-ab () () (= (*T) ({|} x ph) (iota X (*T) (A. x (T) (<-> (e. (cv x) (cv X)) ph))))) stmt (df-v () () (= (*T) (V) ({|} x (= (T) (cv x) (cv x))))) stmt (df-dif () () (= (*T) (\ A B) ({|} x (/\ (e. (cv x) A) (-. (e. (cv x) B)))))) stmt (df-un () () (= (*T) (u. A B) ({|} x (\/ (e. (cv x) A) (e. (cv x) B))))) stmt (df-in () () (= (*T) (i^i A B) ({|} x (/\ (e. (cv x) A) (e. (cv x) B))))) stmt (df-nul () () (= (*T) ({/}) (\ (V) (V)))) stmt (df-sn () () (= (*T) ({} a) ({|} x (= (T) (cv x) a)))) stmt (df-pr () () (= (*T) ({,} a b) (u. ({} a) ({} b)))) stmt (df-ss () () (<-> (C_ A B) (= (*T) (i^i A B) A))) stmt (dfpss2 () () (<-> (C: A B) (/\ (C_ A B) (-. (= (*T) A B)))))