Formal proof of sentence in first-order calculus, example. It is a well-known observation that in every non-empty bar there always is a customer that can rightfully shout "When I drink, everybody drinks." In the first-order logic this is expressed by the sentence$$\exists x(x = x) \supset \exists x(D(x) \supset \forall y D(y)).$$What would a formal proof of this sentence in the first-order calculus look like?
The textbook I am using does not have a whole lot of examples, and it would be enlightening to have a detailed worked out example to have in mind when thinking about related things.
Any help would be appreciated.
 A: I'll prove it with Natural Deduction.
Assuming the "standard" semantics, with non-empty domain for the interpretation, the antecedent $\exists x (x=x)$ is valid; thus, I'll prove only the validity of the consequent :

$\exists x (Dx \to \forall y Dy)$.

Proof :
1) $\lnot\exists x (Dx \to \forall y Dy)$ --- assumed [a]
2) $\lnot Dx$ --- assumed [b]
3) $Dx$ --- assumed [c]
4) $\bot$ --- from 2) and 3) by $(\lnot \text E)$
5) $\forall y Dy$ --- from 4) by $(\bot \text E)$
6) $Dx \to \forall y Dy$ --- from 3) and 5) by $(\to \text I)$, discharging [c]
7) $\exists x (Dx \to \forall y Dy)$ --- from 6) by $(\exists \text I)$
8) $\bot$ --- from 1) and 7) by $(\lnot \text E)$
9) $Dx$ --- from 2) and 8) by $(\text {DN})$ (Double Negation), discharging [b]
10)$\forall y Dy$ --- from 9) by $(\forall \text I)$
11) $Dx \to \forall y Dy$ --- from 10) by $(\to \text I)$
12) $\exists x (Dx \to \forall y Dy)$ --- from 11) by $(\exists \text I)$
13) $\bot$ --- from 1) and 12) by $(\lnot \text E)$

$\exists x (Dx \to \forall y Dy)$ --- from 1) and 13) by $(\text {DN})$, discharging [a].

