Nuprl Definition : l_eqset

l_eqset(T;L1;L2) ==  ∀x:T. ((x ∈ L1) ⇐⇒ (x ∈ L2))


Definitions occuring in Statement :  l_member: (x ∈ l),  all: ∀x:A. B[x],  iff: P ⇐⇒ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  l_member: (x ∈ l)
FDL editor aliases :  l_eqset
Latex:
l\_eqset(T;L1;L2)  ==    \mforall{}x:T.  ((x  \mmember{}  L1)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L2))


Date html generated: 2016_05_14-PM-03_29_22
Last ObjectModification: 2015_09_22-PM-05_59_48

Theory : decidable!equality


Home Index