There is exactly one way to choose 0 elements from the empty set.

0_0_1.v

Parameter set : Set.
Parameter In : (set * set) -> Prop.

Definition subset (A B : set) : Prop :=
  forall x : set, In(x,A) -> In(x,B).

Axiom ZF_extensionality :
  forall X Y : set,
    (forall z : set, In(z,X) <-> In(z,Y))
    -> X = Y.

Axiom ZF_specification :
  forall (P: set -> Prop), forall X : set,
  sig (fun (S : set) =>
    forall z : set,
    In(z,S) <-> (In(z,X) /\ P(z)) ).

Axiom ZF_powerset :
  forall X : set,
  sig (fun (Y : set) =>
    forall Z : set,
    subset Z X -> In(Z,Y) ).

Axiom ZF_pairing :
  forall X Y : set,
  sig (fun (Z : set) =>
    In(X,Z) /\ In(Y,Z) ).

Axiom ZF_emptyset :
  sig (fun (X : set) =>
    forall y : set,
    not(In(y,X)) ).

Lemma proper_powerset : 
  forall X : set,
  sig (fun (Y : set) =>
    forall Z : set,
    subset Z X <-> In(Z,Y) ).
Proof.
  intros.
  destruct (ZF_powerset X) as [px].
  destruct (ZF_specification (fun z => subset z X) px) as [ppx].
  firstorder.
Qed.

Definition subsets_of : set -> set := fun X =>
  proj1_sig (proper_powerset X).

Definition specified (P : set -> Prop) (X : set) : set :=
  proj1_sig (ZF_specification P X).

Definition Empty : set := proj1_sig ZF_emptyset.
Definition Zero : set := Empty.

Lemma one : sig (fun (One : set) => forall z : set, In(z, One) <-> z = Zero).
Proof.
  destruct (ZF_pairing Zero Zero) as [pzz].
  destruct (ZF_specification (fun z => z = Zero) pzz) as [one].
  exists one.
  firstorder.
  rewrite H1.
  firstorder.
Qed.

Definition One : set := proj1_sig one.

Ltac use_properties_of X x :=
  unfold X in *;
  let S := fresh "S" in pose proof (proj2_sig x); remember (proj1_sig x) as S eqn:Seq; clear Seq.

Theorem exactly_one_zero_subset_of_empty_set : (specified (fun s => s = Zero) (subsets_of Empty)) = One.
Proof.
  apply ZF_extensionality.
  intuition.
  all: use_properties_of One one;
       use_properties_of specified (ZF_specification (fun s => s = Zero) (subsets_of Empty));
       unfold Zero in *;
       use_properties_of Empty ZF_emptyset;
       use_properties_of subsets_of (proper_powerset S0).
  { apply H0.
    apply ZF_extensionality.
    pose proof (H1 z).
    intuition;
    rewrite <- H7 in *;
    trivial. }
  { assert (zZ : z = S1) by firstorder.
    rewrite zZ.
    apply H1.
    intuition.
    apply (proj2_sig (proper_powerset S1)).
    unfold subset; trivial. }
Qed.

Check exactly_one_zero_subset_of_empty_set.