Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012) (Proof shortened by AV, 7-Apr-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ralsng.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
Assertion | rexsng | |- ( A e. V -> ( E. x e. { A } ph <-> ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralsng.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
2 | nfv | |- F/ x ps |
|
3 | 2 1 | rexsngf | |- ( A e. V -> ( E. x e. { A } ph <-> ps ) ) |