Nuprl Definition : m-set

m-set(X;d;x.A[x]) ==  ∀x,y:X.  (x ≡ y ⇒ (A[x] ⇐⇒ A[y]))


Definitions occuring in Statement :  meq: x ≡ y,  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  implies: P ⇒ Q
FDL editor aliases :  m-set
Latex:
m-set(X;d;x.A[x])  ==    \mforall{}x,y:X.    (x  \mequiv{}  y  {}\mRightarrow{}  (A[x]  \mLeftarrow{}{}\mRightarrow{}  A[y]))


Date html generated: 2020_05_20-AM-11_54_36
Last ObjectModification: 2020_01_12-PM-00_26_41

Theory : reals


Home Index