MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralsng Structured version   Unicode version

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
StepHypRef Expression
1 ralsnsg 4064 . 2  |-  ( A  e.  V  ->  ( A. x  e.  { A } ph  <->  [. A  /  x ]. ph ) )
2 ralsng.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32sbcieg 3360 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
41, 3bitrd 253 1  |-  ( A  e.  V  ->  ( A. x  e.  { A } ph  <->  ps ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator