Nuprl Definition : l_all2
(∀x<y∈L.P[x; y]) ==  ∀x,y:T.  (x before y ∈ L 
⇒ P[x; y])
Definitions occuring in Statement : 
l_before: x before y ∈ l
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
l_before: x before y ∈ l
FDL editor aliases : 
l_all2
Latex:
(\mforall{}x<y\mmember{}L.P[x;  y])  ==    \mforall{}x,y:T.    (x  before  y  \mmember{}  L  {}\mRightarrow{}  P[x;  y])
Date html generated:
2016_05_15-PM-01_55_51
Last ObjectModification:
2015_09_23-AM-07_37_28
Theory : list!
Home
Index