Theorem eubi

Description: Equivalence theorem for the unique existential quantifier. Theorem *14.271 in WhiteheadRussell p. 192. (Contributed by Andrew Salmon, 11-Jul-2011) Reduce dependencies on axioms. (Revised by BJ, 7-Oct-2022)

	Ref	Expression
Assertion	eubi	|- ( A. x ( ph <-> ps ) -> ( E! x ph <-> E! x ps ) )

Proof

Step	Hyp	Ref	Expression
1		exbi	|- ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) )
2		mobi	|- ( A. x ( ph <-> ps ) -> ( E* x ph <-> E* x ps ) )
3	1 2	anbi12d	|- ( A. x ( ph <-> ps ) -> ( ( E. x ph /\ E* x ph ) <-> ( E. x ps /\ E* x ps ) ) )
4		df-eu	|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
5		df-eu	|- ( E! x ps <-> ( E. x ps /\ E* x ps ) )
6	3 4 5	3bitr4g	|- ( A. x ( ph <-> ps ) -> ( E! x ph <-> E! x ps ) )