En clase el profesor nos esta enunciando los axiomas de ZF en un lenguaje de primer orden, entonces por que las demostraciones de unicidad y esas cosas se dan de una manera infomral, no deberia de darse a travez del calculo de predicados? y como seria la prueba de .... por ejemplo la unicidad del conjunto vacio de manera formal???

Gracias...

Buena observación Fernando!!!
Pues las pruebas formales de la unicidad vienen como tarea.

Mañana hacemos en clase una de estas pruebas. recuerdame al inicio.

pero formalmente demostramos que hay a lo mas uno que cumple el no tener elementos, afuera del sistema formal uno dice: bueno pues entonces ya esta, pero dentro del sistema formal ya se demostro que ese monito cuyo a lo mas hay uno es el que su existencia es garantizada por el axioma 2?

Por el momento, para la tarea, nos quedaremos con la idea de que la conjuncion de las siguientes proposiciones (dada una propiedad P(x)) expresa la existencia y unicidad de un conjunto que cumpla la propiedad P(x) :
1. Existe y tal que P(y).
2. Para cualesquiera u,v, si se tiene que P(u) syss P(v), entonces u=v.