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

Theorem dfsbcq2 3007
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 1639 and substitution for class variables df-sbc 3005. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3006. (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 2356 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2283 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 3005 . . 3  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
43bicomi 193 . 2  |-  ( A  e.  { x  | 
ph }  <->  [. A  /  x ]. ph )
51, 2, 43bitr3g 278 1  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   [wsb 1638    e. wcel 1696   {cab 2282   [.wsbc 3004
This theorem is referenced by:  sbsbc  3008  sbc8g  3011  sbc2or  3012  sbceq1a  3014  sbc5  3028  sbcng  3044  sbcimg  3045  sbcan  3046  sbcang  3047  sbcor  3048  sbcorg  3049  sbcbig  3050  sbcal  3051  sbcalg  3052  sbcex2  3053  sbcexg  3054  sbc3ang  3062  sbcel1gv  3063  sbcel2gv  3064  sbctt  3066  sbcralt  3076  sbcralg  3078  sbcrexg  3079  sbcreug  3080  rspsbc  3082  rspesbca  3084  sbcel12g  3109  sbceqg  3110  csbifg  3606  sbcbrg  4088  csbopabg  4110  opelopabsb  4291  onminex  4614  findes  4702  iota4  5253  csbiotag  5264  csbriotag  6333  nn0ind-raph  10128  uzind4s  10294  iuninc  23174  measiuns  23559
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-clab 2283  df-cleq 2289  df-clel 2292  df-sbc 3005
  Copyright terms: Public domain W3C validator