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

Metamath Proof Explorer

Theorem ralsng

Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2015) Avoid ax-10 , ax-12 . (Revised by GG, 30-Sep-2024)

Ref Expression
Hypothesis ralsng.1 
|- ( x = A -> ( ph <-> ps ) )
Assertion ralsng 
|- ( A e. V -> ( A. x e. { A } ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 ralsng.1 
 |-  ( x = A -> ( ph <-> ps ) )
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 elisset 
 |-  ( A e. V -> E. x x = A )
8 1 pm5.74i 
 |-  ( ( x = A -> ph ) <-> ( x = A -> ps ) )
9 8 albii 
 |-  ( A. x ( x = A -> ph ) <-> A. x ( x = A -> ps ) )
10 9 a1i 
 |-  ( E. x x = A -> ( A. x ( x = A -> ph ) <-> A. x ( x = A -> ps ) ) )
11 19.23v 
 |-  ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) )
12 11 a1i 
 |-  ( E. x x = A -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )
13 pm5.5 
 |-  ( E. x x = A -> ( ( E. x x = A -> ps ) <-> ps ) )
14 10 12 13 3bitrd 
 |-  ( E. x x = A -> ( A. x ( x = A -> ph ) <-> ps ) )
15 7 14 syl 
 |-  ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
16 6 15 bitrid 
 |-  ( A e. V -> ( A. x e. { A } ph <-> ps ) )