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

Theorem dfsbcq2 3327
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 1745 and substitution for class variables df-sbc 3325. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3326. (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 2526 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2440 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 3325 . . 3  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
43bicomi 202 . 2  |-  ( A  e.  { x  | 
ph }  <->  [. A  /  x ]. ph )
51, 2, 43bitr3g 287 1  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398   [wsb 1744    e. wcel 1823   {cab 2439   [.wsbc 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3325
This theorem is referenced by:  sbsbc  3328  sbc8g  3332  sbc2or  3333  sbceq1a  3335  sbc5  3349  sbcng  3365  sbcimg  3366  sbcan  3367  sbcor  3368  sbcbig  3369  sbcal  3374  sbcex2  3375  sbcel1v  3383  sbctt  3387  sbcralt  3397  sbcreu  3401  rspsbc  3403  rspesbca  3405  sbcel12  3822  sbceqg  3823  csbif  3979  sbcbr123  4490  opelopabsb  4746  csbopab  4768  csbopabgALT  4769  iota4  5552  csbiota  5563  csbriota  6244  onminex  6615  findes  6703  nn0ind-raph  10960  uzind4s  11142  nn0min  27845  sbcrexgOLD  30958  sbcangOLD  33690  sbcorgOLD  33691  sbcalgOLD  33703  sbcexgOLD  33704  sbcel12gOLD  33705  sbcel1gvOLD  34059
  Copyright terms: Public domain W3C validator