This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexsng

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012) Avoid ax-10 , ax-12 . (Revised by GG, 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 ) )