Metamath Proof Explorer

Theorem eupickb

Description: Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994) (Proof shortened by Wolf Lammen, 27-Dec-2018)

		Ref	Expression
	Assertion	eupickb	$⊢ (\exists! x φ \land \exists! x ψ \land \exists x (φ \land ψ)) \to (φ \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		eupick	$⊢ (\exists! x φ \land \exists x (φ \land ψ)) \to (φ \to ψ)$
2	1	3adant2	$⊢ (\exists! x φ \land \exists! x ψ \land \exists x (φ \land ψ)) \to (φ \to ψ)$
3		exancom	$⊢ \exists x (φ \land ψ) \leftrightarrow \exists x (ψ \land φ)$
4		eupick	$⊢ (\exists! x ψ \land \exists x (ψ \land φ)) \to (ψ \to φ)$
5	3 4	sylan2b	$⊢ (\exists! x ψ \land \exists x (φ \land ψ)) \to (ψ \to φ)$
6	5	3adant1	$⊢ (\exists! x φ \land \exists! x ψ \land \exists x (φ \land ψ)) \to (ψ \to φ)$
7	2 6	impbid	$⊢ (\exists! x φ \land \exists! x ψ \land \exists x (φ \land ψ)) \to (φ \leftrightarrow ψ)$