Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2015) (Proof shortened by AV, 7-Apr-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ralsng.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
Assertion | ralsng | |- ( A e. V -> ( A. x e. { A } ph <-> ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralsng.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
2 | nfv | |- F/ x ps |
|
3 | 2 1 | ralsngf | |- ( A e. V -> ( A. x e. { A } ph <-> ps ) ) |