Theorem ralsng 3977

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

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   e. wcel 1872   A.wral 2714   [.wsbc 3242   {csn 3941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-ral 2719  df-v 3024  df-sbc 3243  df-sn 3942

This theorem is referenced by:  2ralsng  3979  ralsn  3981  ralprg  3992  raltpg  3994  ralunsn  4150  iinxsng  4322  frirr  4773  posn  4865  frsn  4867  f12dfv  6131  ranksnb  8250  mgm1  16443  sgrp1  16477  mnd1  16520  mnd1OLD  16521  grp1  16701  cntzsnval  16921  abl1  17447  srgbinomlem4  17719  ring1  17773  mat1dimmul  19443  ufileu  20876  istrkg3ld  24451  cusgra1v  25131  cusgra2v  25132  dfconngra1  25341  1conngra  25345  wwlknext  25394  clwwlkn2  25445  wwlkext2clwwlk  25473  rusgrasn  25615  frgra1v  25668  poimirlem26  31873  poimirlem27  31874  poimirlem31  31878  zlidlring  39529  linds0  39861  snlindsntor  39867  lmod1  39888