 Solution

Line	Context	Formula	Justification
1	${1}$	$\exists x (Q (x) \land \forall y (Q (y) \to y = x))$	Premise
2	${1, 2}$	$Q (a) \land \forall y (Q (y) \to y = a)$	Temporary assumption
3	${1, 2}$	$Q (a)$	conjunction elimination rule $\land -elim-L$ on 2
4	${1, 2}$	$\forall y (Q (y) \to y = a)$	conjunction elimination rule $\land -elim-R$ on 2
5	${1, 2}$	$Q (b) \to b = a$	universal elimination $\forall -elim$ on 4; instantiate at $b$
6	${1, 2, 6}$	$b = a$	Temporary assumption
7	${1, 2, 6}$	$b = b$	equality introduction rule $= -intro$
8	${1, 2, 6}$	$a = b$	equality elimination rule $= -elim$ on 6, 7
9	${1, 2, 6}$	$Q (b)$	equality elimination rule $= -elim$ on 8, 3
10	${1, 2}$	$b = a \to Q (b)$	implication introduction rule $\to -intro$ on 9; discharge 6
11	${1, 2}$	$Q (b) \leftrightarrow b = a$	biconditional introduction rule $\leftrightarrow -intro$ on 5, 10
12	${1, 2}$	$\forall y (Q (y) \leftrightarrow y = a)$	universal introduction $\forall -intro$ on 11; $b$ fresh
13	${1, 2}$	$\exists x \forall y (Q (y) \leftrightarrow y = x)$	existential quantifier introduction rule $\exists -intro$ on 12; witness $a$
14	${1}$	$\exists x \forall y (Q (y) \leftrightarrow y = x)$	existential quantifier elimination rule $\exists -elim$ on 1, 13; discharge 2; $a$ fresh

Here

b

is absent from every open assumption when line 12 uses universal introduction. In line 13 the existential quantifier binds the witness position occupied by

a

; the conclusion then has no free

a

, allowing line 14 to close its witness subproof. Hence

\exists x (Q (x) \land \forall y (Q (y) \to y = x)) ⊢ \exists x \forall y (Q (y) \leftrightarrow y = x) .

The premise says an object satisfying

Q

exists and every object satisfying

Q

equals it. The logical biconditional adds the converse explicitly: every object equal to that witness also satisfies

Q

 New to topics? Read the docs here!