Metamath Proof Explorer

Theorem reupick2

Description: Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

		Ref	Expression
	Assertion	reupick2	$⊢ ((\forall x \in A (ψ \to φ) \land \exists x \in A ψ \land \exists! x \in A φ) \land x \in A) \to (φ \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		ancr	$⊢ (ψ \to φ) \to (ψ \to (φ \land ψ))$
2	1	ralimi	$⊢ \forall x \in A (ψ \to φ) \to \forall x \in A (ψ \to (φ \land ψ))$
3		rexim	$⊢ \forall x \in A (ψ \to (φ \land ψ)) \to (\exists x \in A ψ \to \exists x \in A (φ \land ψ))$
4	2 3	syl	$⊢ \forall x \in A (ψ \to φ) \to (\exists x \in A ψ \to \exists x \in A (φ \land ψ))$
5		reupick3	$⊢ (\exists! x \in A φ \land \exists x \in A (φ \land ψ) \land x \in A) \to (φ \to ψ)$
6	5	3exp	$⊢ \exists! x \in A φ \to (\exists x \in A (φ \land ψ) \to (x \in A \to (φ \to ψ)))$
7	6	com12	$⊢ \exists x \in A (φ \land ψ) \to (\exists! x \in A φ \to (x \in A \to (φ \to ψ)))$
8	4 7	syl6	$⊢ \forall x \in A (ψ \to φ) \to (\exists x \in A ψ \to (\exists! x \in A φ \to (x \in A \to (φ \to ψ))))$
9	8	3imp1	$⊢ ((\forall x \in A (ψ \to φ) \land \exists x \in A ψ \land \exists! x \in A φ) \land x \in A) \to (φ \to ψ)$
10		rsp	$⊢ \forall x \in A (ψ \to φ) \to (x \in A \to (ψ \to φ))$
11	10	3ad2ant1	$⊢ (\forall x \in A (ψ \to φ) \land \exists x \in A ψ \land \exists! x \in A φ) \to (x \in A \to (ψ \to φ))$
12	11	imp	$⊢ ((\forall x \in A (ψ \to φ) \land \exists x \in A ψ \land \exists! x \in A φ) \land x \in A) \to (ψ \to φ)$
13	9 12	impbid	$⊢ ((\forall x \in A (ψ \to φ) \land \exists x \in A ψ \land \exists! x \in A φ) \land x \in A) \to (φ \leftrightarrow ψ)$