Nuprl Definition : all
∀x:A. B[x] == x:A ⟶ B[x]
Definitions occuring in Statement :
function: x:A ⟶ B[x]
Definitions occuring in definition :
function: x:A ⟶ B[x]
Rules referencing :
functionUniverseElim,
productUniverseElim,
barInduction,
bar_Induction,
strong_bar_Induction,
StrongContinuity2,
allFunctionality,
allLevelFunctionality
FDL editor aliases :
axm
all
Latex:
\mforall{}x:A. B[x] == x:A {}\mrightarrow{} B[x]
Date html generated:
2016_05_13-PM-03_04_21
Last ObjectModification:
2015_09_22-PM-05_43_40
Theory : core_1
Home
Index