Proving that inclusion is antisymmetric in Coq

Question

I'm a Coq newbie and I'd like to prove that the inclusion relation is antisymmetric, that is: $\forall x\forall y(x\subseteq y\land y\subseteq x\rightarrow x=y)$.

I wrote the following thing:

Section Test.
Variable set : Type.
Variable element : set -> set -> Prop.
Definition subset (x:set) (y:set) := forall z:set, element z x -> element z y.
Axiom equality : forall x y:set, x = y <-> forall z:set, element z x <-> element z y.
Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -> x = y.
Proof.
intros a b.
unfold subset.
intro H.
destruct H as [H0 H1].

At this point I get the following output:

1 subgoal
set : Type
element : set -> set -> Prop
a : set
b : set
H0 : forall z : set, element z a -> element z b
H1 : forall z : set, element z b -> element z a
______________________________________(1/1)
a = b

I'm stuck now because I don't know how to:

• change the goal from $a=b$ to $\forall z(z\in a\leftrightarrow z\in b)$ and then to $c\in a\leftrightarrow c\in b$
• change H0 from $\forall z(z\in a\rightarrow z\in b)$ to $c\in a\rightarrow c\in b$
• change H1 from $\forall z(z\in b\rightarrow z\in c)$ to $c\in b\rightarrow c\in a$

That is, I know how to prove this theorem on paper but not with Coq.

Answer 1

Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -> x = y.
Proof.
  firstorder using equality.
Qed.

Answer 2

An alternative answer, that only uses basic tactics:

Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -> x = y. Proof. intros x y H. inversion H. apply equality. split. apply H0. apply H1. Qed.

For those that don't want to run it through Coq, the proof is fairly obvious, the equality axiom is literally the antecedent subset x y /\ subset y x with a little bit of obfuscation (the quantification is in sort of the wrong spot, and we can effectively move it with the split).