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

Theorem dfsbcq2 3151
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 1659 and substitution for class variables df-sbc 3149. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3150. (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 2490 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2417 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 3149 . . 3  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
43bicomi 194 . 2  |-  ( A  e.  { x  | 
ph }  <->  [. A  /  x ]. ph )
51, 2, 43bitr3g 279 1  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   [wsb 1658    e. wcel 1725   {cab 2416   [.wsbc 3148
This theorem is referenced by:  sbsbc  3152  sbc8g  3155  sbc2or  3156  sbceq1a  3158  sbc5  3172  sbcng  3188  sbcimg  3189  sbcan  3190  sbcang  3191  sbcor  3192  sbcorg  3193  sbcbig  3194  sbcal  3195  sbcalg  3196  sbcex2  3197  sbcexg  3198  sbc3ang  3206  sbcel1gv  3207  sbctt  3210  sbcralt  3220  sbcralg  3222  sbcrexg  3223  sbcreug  3224  rspsbc  3226  rspesbca  3228  sbcel12g  3253  sbceqg  3254  csbifg  3754  sbcbrg  4248  csbopabg  4270  opelopabsb  4452  onminex  4773  findes  4861  iota4  5422  csbiotag  5433  csbriotag  6548  nn0ind-raph  10354  uzind4s  10520
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-clab 2417  df-cleq 2423  df-clel 2426  df-sbc 3149
  Copyright terms: Public domain W3C validator