Theorem ralsng 4023

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 4020	. 2 |- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) )
2		ralsng.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	sbcieg 3327	. 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 1370   e. wcel 1758   A.wral 2799   [.wsbc 3294   {csn 3988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2804  df-v 3080  df-sbc 3295  df-sn 3989

This theorem is referenced by:  ralsn  4026  ralprg  4036  raltpg  4038  ralunsn  4190  iinxsng  4358  frirr  4808  posn  5018  frsn  5020  ranksnb  8148  wrdeqswrdlsw  12464  cntzsnval  15964  srgbinomlem4  16767  ufileu  19627  cusgra1v  23541  cusgra2v  23542  dfconngra1  23729  1conngra  23733  f12dfv  30314  wwlknext  30524  clwwlkn2  30606  wwlkext2clwwlk  30633  rusgrasn  30725  rusgranumwlkl1  30727  frgra1v  30758  mat0dimcrng  31052  mat1dimmul  31058  linds0  31151  snlindsntor  31157  mnd1  31173  grp1  31174  abl1  31175  rng1  31177  lmod1  31186