Nuprl Definition : eq_pair
a =b b == ((fst(a)) (=b) (fst(b))) ∧b ((snd(a)) (=b) (snd(b)))
Definitions occuring in Statement :
set_eq: =b,
band: p ∧b q,
infix_ap: x f y,
pi1: fst(t),
pi2: snd(t)
Definitions occuring in definition :
band: p ∧b q,
pi1: fst(t),
infix_ap: x f y,
set_eq: =b,
pi2: snd(t)
Latex:
a =\msubb{} b == ((fst(a)) (=\msubb{}) (fst(b))) \mwedge{}\msubb{} ((snd(a)) (=\msubb{}) (snd(b)))
Date html generated:
2016_05_15-PM-00_05_39
Last ObjectModification:
2015_09_23-AM-06_24_08
Theory : sets_1
Home
Index