Nuprl Lemma : mFOLisAll_wf

[A:mFOL()]. (mFOLisAll(A) ∈ 𝔹)


Proof




Definitions occuring in Statement :  mFOLisAll: mFOLisAll(A) mFOL: mFOL() bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Lemmas :  mFOquant?_wf bool_wf eqtt_to_assert mFOquant-isall_wf mFOL_wf
\mforall{}[A:mFOL()].  (mFOLisAll(A)  \mmember{}  \mBbbB{})



Date html generated: 2015_07_17-AM-07_54_53
Last ObjectModification: 2015_01_27-AM-10_05_59

Home Index