Theorem ralsng 4067

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 4064	. 2 |- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) )
2		ralsng.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	sbcieg 3360	. 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 1395   e. wcel 1819   A.wral 2807   [.wsbc 3327   {csn 4032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-v 3111  df-sbc 3328  df-sn 4033

This theorem is referenced by:  2ralsng  4069  ralsn  4071  ralprg  4081  raltpg  4083  ralunsn  4239  iinxsng  4412  frirr  4865  posn  5077  frsn  5079  f12dfv  6180  ranksnb  8262  mgm1  16011  sgrp1  16045  mnd1  16088  mnd1OLD  16089  grp1  16269  cntzsnval  16489  abl1  16999  srgbinomlem4  17321  ring1  17375  mat1dimmul  19105  ufileu  20546  cusgra1v  24588  cusgra2v  24589  dfconngra1  24798  1conngra  24802  wwlknext  24851  clwwlkn2  24902  wwlkext2clwwlk  24930  rusgrasn  25072  frgra1v  25125  zlidlring  32878  linds0  33210  snlindsntor  33216  lmod1  33237