consider a being set ;
P₁[a] by A1;
hence ex a being set st P₁[a] ; :: thesis: verum