Theorem rexsng

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012) Avoid ax-10 , ax-12 . (Revised by Gino Giotto, 30-Sep-2024)

	Ref	Expression
Hypothesis	ralsng.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	rexsng	|- ( A e. V -> ( E. x e. { A } ph <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		ralsng.1	|- ( x = A -> ( ph <-> ps ) )
2	1	notbid	|- ( x = A -> ( -. ph <-> -. ps ) )
3	2	ralsng	|- ( A e. V -> ( A. x e. { A } -. ph <-> -. ps ) )
4		dfrex2	|- ( E. x e. { A } ph <-> -. A. x e. { A } -. ph )
5		bicom1	|- ( ( A. x e. { A } -. ph <-> -. ps ) -> ( -. ps <-> A. x e. { A } -. ph ) )
6	5	con1bid	|- ( ( A. x e. { A } -. ph <-> -. ps ) -> ( -. A. x e. { A } -. ph <-> ps ) )
7	4 6	bitrid	|- ( ( A. x e. { A } -. ph <-> -. ps ) -> ( E. x e. { A } ph <-> ps ) )
8	3 7	syl	|- ( A e. V -> ( E. x e. { A } ph <-> ps ) )