Definitions ElisTarskiPf A Sections NuprlLIB Doc

Some definitions of interest.
iff Def P Q == (P Q) & (P Q)
Thm* A,B:Prop. (A B) Prop
not Def A == A False
Thm* A:Prop. (A) Prop
repst Def x = y == x = y
Thm* t,x:Term. (t = x) Prop
s Def s(t) == SUBX(f(t); f(t))
Thm* t:Term. s(t) Term
subx Def SUBX(t; e) == t[e/X]
Thm* t,r:Term. SUBX(t; r) Term

About:
memberpropimpliesandfalseall!abstraction

Definitions ElisTarskiPf A Sections NuprlLIB Doc