ZF* Minus Extensionality
The attached file presents a full proof of ZF* minus Extensionality interpreting full ZF.
This sketch of this proof had also been posted to MathOverflow at:
Can ZF be interpreted in a theory axiomatized by a version of Replacement and Infinity
Equivalents of Replacement under removal of Extensionality
Is this kind of Predication preserved under co-extensionality