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

Theorem dfsbcq2 3258
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 1806 and substitution for class variables df-sbc 3256. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3257. (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 2537 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2458 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 3256 . . 3  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
43bicomi 207 . 2  |-  ( A  e.  { x  | 
ph }  <->  [. A  /  x ]. ph )
51, 2, 43bitr3g 295 1  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452   [wsb 1805    e. wcel 1904   {cab 2457   [.wsbc 3255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-clab 2458  df-cleq 2464  df-clel 2467  df-sbc 3256
This theorem is referenced by:  sbsbc  3259  sbc8g  3263  sbc2or  3264  sbceq1a  3266  sbc5  3280  sbcng  3296  sbcimg  3297  sbcan  3298  sbcor  3299  sbcbig  3300  sbcal  3305  sbcex2  3306  sbcel1v  3314  sbctt  3318  sbcralt  3328  sbcreu  3332  rspsbc  3334  rspesbca  3336  sbcel12  3776  sbceqg  3777  csbif  3922  sbcbr123  4447  opelopabsb  4711  csbopab  4733  csbopabgALT  4734  iota4  5571  csbiota  5582  csbriota  6282  onminex  6653  findes  6742  nn0ind-raph  11058  uzind4s  11242  nn0min  28459  sbcrexgOLD  35699  sbcangOLD  36960  sbcorgOLD  36961  sbcalgOLD  36973  sbcexgOLD  36974  sbcel12gOLD  36975  sbcel1gvOLD  37318
  Copyright terms: Public domain W3C validator