Metamath Proof Explorer


Theorem ralsnsg

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 ) )

Proof

Step Hyp Ref Expression
1 df-ral
 |-  ( A. x e. { A } ph <-> A. x ( x e. { A } -> ph ) )
2 velsn
 |-  ( x e. { A } <-> x = A )
3 2 imbi1i
 |-  ( ( x e. { A } -> ph ) <-> ( x = A -> ph ) )
4 3 albii
 |-  ( A. x ( x e. { A } -> ph ) <-> A. x ( x = A -> ph ) )
5 1 4 bitri
 |-  ( A. x e. { A } ph <-> A. x ( x = A -> ph ) )
6 sbc6g
 |-  ( A e. V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )
7 5 6 bitr4id
 |-  ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) )