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

Theorem dfsbcq2 2924
Description: This theorem, which is similar to Theorem 6.7 of [Quine] p. 42 and holds under both our definition and Quine's, relates logic substitution df-sb 1883 and substitution for class variables df-sbc 2922. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2923. (Contributed by NM, 31-Dec-2016.)
Assertion
Ref Expression
dfsbcq2  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2313 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2240 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 2922 . . 3  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
43bicomi 195 . 2  |-  ( A  e.  { x  | 
ph }  <->  [. A  /  x ]. ph )
51, 2, 43bitr3g 280 1  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1619    e. wcel 1621   [wsb 1882   {cab 2239   [.wsbc 2921
This theorem is referenced by:  sbsbc  2925  sbc8g  2928  sbc2or  2929  sbceq1a  2931  sbc5  2945  sbcng  2961  sbcimg  2962  sbcan  2963  sbcang  2964  sbcor  2965  sbcorg  2966  sbcbig  2967  sbcal  2968  sbcalg  2969  sbcex2  2970  sbcexg  2971  sbc3ang  2979  sbcel1gv  2980  sbcel2gv  2981  sbctt  2983  sbcralt  2993  sbcralg  2995  sbcrexg  2996  sbcreug  2997  ra4sbc  2999  ra4esbca  3001  sbcel12g  3024  sbceqg  3025  csbifg  3498  sbcbrg  3969  csbopabg  3991  opelopabsb  4168  onminex  4489  findes  4577  iota4  6161  csbriotag  6203  nn0ind-raph  9991  uzind4s  10157
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-clab 2240  df-cleq 2246  df-clel 2249  df-sbc 2922
  Copyright terms: Public domain W3C validator