Nuprl - DiscreteMath LEMMAs for delete_fenum_value_is_fenum

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
3	Thm* Bij({u:\| P(u) }; {v:\| Q(v) }; f) Thm* Thm* (m:{u:\| P(u) }, k:{v:\| Q(v) }. Thm* (Bij({u:\| P(u) & u = m }; {v:\| Q(v) & v = k }; Thm* (Bij(Replace value k by f(m) in f))	[delete_fenum_value_is_fenum_gen]
cites the following:
2	Thm* Inj({u:\| P(u) }; {v:\| Q(v) }; f) Thm* Thm* (m:{u:\| P(u) }, k:{v:\| Q(v) }. Thm* (Inj({u:\| P(u) & u = m }; {v:\| Q(v) & v = k }; Thm* (Inj(Replace value k by f(m) in f))	[delete_fenum_value_is_inj_gen]
0	Thm* Inj({u:\| P(u) }; {u:\| Q(u) }; f) Thm* Thm* (m:{u:\| P(u) }, k:{v:\| Q(v) }, i:{u:\| P(u) & u = m }. Thm* (f(i) = k Thm* ( Thm* ((Replace value k by f(m) in f)(i) = f(m) {v:\| Q(v) & v = k })	[delete_fenum_value_comp1_gen]
0	Thm* Inj({u:\| P(u) }; {u:\| Q(u) }; f) Thm* Thm* (m:{u:\| P(u) }, k:{v:\| Q(v) }, i:{u:\| P(u) & u = m }. Thm* (f(i) = k Thm* ( Thm* ((Replace value k by f(m) in f)(i) = f(i) {v:\| Q(v) & v = k })	[delete_fenum_value_comp2_gen]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html