Theorem ralsng 4218

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

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   A.wral 2912   [.wsbc 3435   {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:  2ralsng  4220  ralsn  4222  ralprg  4234  raltpg  4236  ralunsn  4422  iinxsng  4600  frirr  5091  posn  5187  frsn  5189  f12dfv  6529  ranksnb  8690  mgm1  17257  sgrp1  17293  mnd1  17331  grp1  17522  cntzsnval  17757  abl1  18269  srgbinomlem4  18543  ring1  18602  mat1dimmul  20282  ufileu  21723  istrkg3ld  25360  1hevtxdg0  26401  wlkp1lem8  26577  wwlksnext  26788  wwlksext2clwwlk  26924  dfconngr1  27048  1conngr  27054  frgr1v  27135  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  zlidlring  41928  linds0  42254  snlindsntor  42260  lmod1  42281