Nuprl Definition : predicate_equivalent
P1 ⇐⇒ P2 == ∀x:T. (P1 x ⇐⇒ P2 x)
Definitions occuring in Statement :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a
FDL editor aliases :
predicate_equivalent
Latex:
P1 \mLeftarrow{}{}\mRightarrow{} P2 == \mforall{}x:T. (P1 x \mLeftarrow{}{}\mRightarrow{} P2 x)
Date html generated:
2016_05_14-AM-06_05_41
Last ObjectModification:
2015_09_22-PM-05_46_55
Theory : relations
Home
Index