Theorem ralsng 4018

Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)

Hypothesis

Ref	Expression
ralsng.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

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

Distinct variable groups:   x, A   ps, x

Allowed substitution hints:   ph( x)   V( x)

Proof of Theorem ralsng

Step	Hyp	Ref	Expression
1		ralsnsg 4015	. 2 |- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) )
2		ralsng.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	sbcieg 3312	. 2 |- ( A e. V -> ( [. A / x ]. ph <-> ps ) )
4	1, 3	bitrd 261	1 |- ( A e. V -> ( A. x e. { A } ph <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1455   e. wcel 1898   A.wral 2749   [.wsbc 3279   {csn 3980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-ral 2754  df-v 3059  df-sbc 3280  df-sn 3981

This theorem is referenced by:  2ralsng  4020  ralsn  4022  ralprg  4033  raltpg  4035  ralunsn  4200  iinxsng  4372  frirr  4830  posn  4922  frsn  4924  f12dfv  6197  ranksnb  8324  mgm1  16549  sgrp1  16583  mnd1  16626  mnd1OLD  16627  grp1  16807  cntzsnval  17027  abl1  17553  srgbinomlem4  17825  ring1  17879  mat1dimmul  19550  ufileu  20983  istrkg3ld  24558  cusgra1v  25238  cusgra2v  25239  dfconngra1  25448  1conngra  25452  wwlknext  25501  clwwlkn2  25552  wwlkext2clwwlk  25580  rusgrasn  25722  frgra1v  25775  poimirlem26  32011  poimirlem27  32012  poimirlem31  32016  dfconngr1  39929  1conngr  39935  zlidlring  40201  linds0  40531  snlindsntor  40537  lmod1  40558