reupick3

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

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

Step	Hyp	Ref	Expression
1		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
2		df-rex	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow \exists x (x \in A \land (φ \land ψ))$
3		anass	$⊢ ((x \in A \land φ) \land ψ) \leftrightarrow (x \in A \land (φ \land ψ))$
4	3	exbii	$⊢ \exists x ((x \in A \land φ) \land ψ) \leftrightarrow \exists x (x \in A \land (φ \land ψ))$
5	2 4	bitr4i	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow \exists x ((x \in A \land φ) \land ψ)$
6		eupick	$⊢ (\exists! x (x \in A \land φ) \land \exists x ((x \in A \land φ) \land ψ)) \to ((x \in A \land φ) \to ψ)$
7	1 5 6	syl2anb	$⊢ (\exists! x \in A φ \land \exists x \in A (φ \land ψ)) \to ((x \in A \land φ) \to ψ)$
8	7	expd	$⊢ (\exists! x \in A φ \land \exists x \in A (φ \land ψ)) \to (x \in A \to (φ \to ψ))$
9	8	3impia	$⊢ (\exists! x \in A φ \land \exists x \in A (φ \land ψ) \land x \in A) \to (φ \to ψ)$

Metamath Proof Explorer