Nuprl Definition : fpf-all
∀x∈dom(f). v=f(x) ⇒ P[x; v] == ∀x:A. ((↑x ∈ dom(f)) ⇒ P[x; f(x)])
Definitions occuring in Statement :
fpf-ap: f(x),
fpf-dom: x ∈ dom(f),
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
fpf-all
\mforall{}x\mmember{}dom(f). v=f(x) {}\mRightarrow{} P[x; v] == \mforall{}x:A. ((\muparrow{}x \mmember{} dom(f)) {}\mRightarrow{} P[x; f(x)])
Date html generated:
2015_07_17-AM-11_10_14
Last ObjectModification:
2012_02_25-AM-11_10_55
Home
Index