Theorem exexw

Description: Existential quantification is idempotent. Weak version of bj-exexbiex , requiring fewer axioms. (Contributed by Gino Giotto, 4-Nov-2024)

	Ref	Expression
Hypothesis	exexw.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	exexw	|- ( E. x ph <-> E. x E. x ph )

Proof

Step	Hyp	Ref	Expression
1		exexw.1	|- ( x = y -> ( ph <-> ps ) )
2	1	notbid	|- ( x = y -> ( -. ph <-> -. ps ) )
3	2	hba1w	|- ( A. x -. ph -> A. x A. x -. ph )
4	2	spw	|- ( A. x -. ph -> -. ph )
5	4	alimi	|- ( A. x A. x -. ph -> A. x -. ph )
6	3 5	impbii	|- ( A. x -. ph <-> A. x A. x -. ph )
7	6	notbii	|- ( -. A. x -. ph <-> -. A. x A. x -. ph )
8		df-ex	|- ( E. x ph <-> -. A. x -. ph )
9		2exnaln	|- ( E. x E. x ph <-> -. A. x A. x -. ph )
10	7 8 9	3bitr4i	|- ( E. x ph <-> E. x E. x ph )