Theorem ralsng 4062

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 4059	. 2 |- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) )
2		ralsng.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	sbcieg 3364	. 2 |- ( A e. V -> ( [. A / x ]. ph <-> ps ) )
4	1, 3	bitrd 253	1 |- ( A e. V -> ( A. x e. { A } ph <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767   A.wral 2814   [.wsbc 3331   {csn 4027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-v 3115  df-sbc 3332  df-sn 4028

This theorem is referenced by:  2ralsng  4064  ralsn  4066  ralprg  4076  raltpg  4078  ralunsn  4233  iinxsng  4402  frirr  4856  posn  5068  frsn  5070  f12dfv  6168  ranksnb  8246  wrdeqswrdlsw  12640  mnd1  15783  grp1  15956  cntzsnval  16176  abl1  16687  srgbinomlem4  17008  rng1  17061  mat0dimcrng  18779  mat1dimmul  18785  ufileu  20247  cusgra1v  24234  cusgra2v  24235  dfconngra1  24444  1conngra  24448  wwlknext  24497  clwwlkn2  24548  wwlkext2clwwlk  24576  rusgrasn  24718  rusgranumwlkl1  24720  frgra1v  24771  linds0  32364  snlindsntor  32370  lmod1  32391