Nuprl Definition : member
t ∈ T == t = t ∈ T
Definitions occuring in Statement :
equal: s = t ∈ T
Definitions occuring in definition :
equal: s = t ∈ T
Rules referencing :
imageEqInduction,
pointwiseFunctionalityForEquality,
barInduction,
bar_Induction,
strong_bar_Induction,
Continuity,
StrongContinuity2,
divergentSqle,
divergentSqlen,
pointwiseFunctionality wrename,
hypothesis_subsumption,
freeFromAtom1Atom2,
freeFromAtomSet,
callbyvalueInt,
callbyvalueAtom1,
callbyvalueAtom2,
callbyvalueAtom,
callbyvalueType,
callbyvalueAdd,
callbyvalueMultiply,
callbyvalueDivide,
callbyvalueRemainder,
callbyvalueMinus,
callbyvalueLess,
callbyvalueIntEq,
callbyvalueAtomEq,
callbyvalueAtomnEq,
applyInt,
callbyvalueSpread,
callbyvalueDecide,
exceptionSqequal,
exceptionLess,
exceptionInteq,
exceptionAtomeq,
exceptionAtomeq1,
exceptionAtomeq2,
exceptionAdd,
exceptionMultiply,
exceptionDivide,
exceptionRemainder,
ispairExceptionCases,
isintExceptionCases,
isaxiomExceptionCases,
isatomExceptionCases,
isinlExceptionCases,
isinrExceptionCases,
islambdaExceptionCases,
isatom1ExceptionCases,
isatom2ExceptionCases,
decideExceptionCases,
spreadExceptionCases,
minusExceptionCases,
applyExceptionCases,
int_eqExceptionCases,
lessExceptionCases,
atom_eqExceptionCases,
atom1_eqExceptionCases,
atom2_eqExceptionCases,
addExceptionCases,
divideExceptionCases,
remainderExceptionCases,
multiplyExceptionCases,
callbyvalueExceptionCases,
ispairCases,
isintCases,
isatomCases,
isaxiomCases,
islambdaCases,
isinlCases,
isinrCases,
isatom1Cases,
isatom2Cases,
lessCases,
pertypeEquality,
pertypeMemberEquality,
pertypeElimination,
existsFunctionality,
allLevelFunctionality,
uallLevelFunctionality,
existsLevelFunctionality,
andLevelFunctionality,
orLevelFunctionality,
orFunctionality,
impliesFunctionality,
impliesLevelFunctionality
FDL editor aliases :
member
Latex:
t \mmember{} T == t = t
Date html generated:
2016_05_13-PM-03_04_06
Last ObjectModification:
2015_09_22-PM-01_26_54
Theory : core_1
Home
Index