Theorem ralsn 4222

Description: Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)

Hypotheses

Ref	Expression
ralsn.1	|- A e. _V
ralsn.2	|- ( x = A -> ( ph <-> ps ) )

Assertion

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

Distinct variable groups:   x, A   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem ralsn

Step	Hyp	Ref	Expression
1		ralsn.1	. 2 |- A e. _V
2		ralsn.2	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	ralsng 4218	. 2 |- ( A e. _V -> ( A. x e. { A } ph <-> ps ) )
4	1, 3	ax-mp 5	1 |- ( A. x e. { A } ph <-> ps )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-sbc 3436  df-sn 4178

This theorem is referenced by:  elixpsn  7947  frfi  8205  dffi3  8337  fseqenlem1  8847  fpwwe2lem13  9464  hashbc  13237  hashf1lem1  13239  eqs1  13392  cshw1  13568  rpnnen2lem11  14953  drsdirfi  16938  0subg  17619  efgsp1  18150  dprd2da  18441  lbsextlem4  19161  ply1coe  19666  mat0dimcrng  20276  txkgen  21455  xkoinjcn  21490  isufil2  21712  ust0  22023  prdsxmetlem  22173  prdsbl  22296  finiunmbl  23312  xrlimcnp  24695  chtub  24937  2sqlem10  25153  dchrisum0flb  25199  pntpbnd1  25275  usgr1e  26137  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  wlkl1loop  26534  crctcshwlkn0lem7  26708  2pthdlem1  26826  rusgrnumwwlkl1  26863  clwwlksn2  26910  clwwlksel  26914  1wlkdlem4  27000  h1deoi  28408  bnj149  30945  subfacp1lem5  31166  cvmlift2lem1  31284  cvmlift2lem12  31296  conway  31910  etasslt  31920  slerec  31923  lindsenlbs  33404  poimirlem28  33437  poimirlem32  33441  heibor1lem  33608