Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ralsnsg | |- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbc6g | |- ( A e. V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) ) |
|
2 | df-ral | |- ( A. x e. { A } ph <-> A. x ( x e. { A } -> ph ) ) |
|
3 | velsn | |- ( x e. { A } <-> x = A ) |
|
4 | 3 | imbi1i | |- ( ( x e. { A } -> ph ) <-> ( x = A -> ph ) ) |
5 | 4 | albii | |- ( A. x ( x e. { A } -> ph ) <-> A. x ( x = A -> ph ) ) |
6 | 2 5 | bitri | |- ( A. x e. { A } ph <-> A. x ( x = A -> ph ) ) |
7 | 1 6 | syl6rbbr | |- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) ) |