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

Theorem ralsng 3672
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 ralsns 3670 . 2  |-  ( A  e.  V  ->  ( A. x  e.  { A } ph  <->  [. A  /  x ]. ph ) )
2 ralsng.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32sbcieg 3023 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
41, 3bitrd 244 1  |-  ( A  e.  V  ->  ( A. x  e.  { A } ph  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1684   A.wral 2543   [.wsbc 2991   {csn 3640
This theorem is referenced by:  ralsn  3674  ralprg  3682  raltpg  3684  ralunsn  3815  iinxsng  3978  frirr  4370  posn  4758  frsn  4760  ranksnb  7499  cntzsnval  14800  ufileu  17614  cbicp  24578  cnfilca  24968  isconcl7a  25517  frgra1v  27538
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-sbc 2992  df-sn 3646
  Copyright terms: Public domain W3C validator