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

Theorem dfsbcq2 3173
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 1661 and substitution for class variables df-sbc 3171. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3172. (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 2503 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2430 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 3171 . . 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 4    <-> wb 178    = wceq 1654   [wsb 1660    e. wcel 1728   {cab 2429   [.wsbc 3170
This theorem is referenced by:  sbsbc  3174  sbc8g  3177  sbc2or  3178  sbceq1a  3180  sbc5  3194  sbcng  3210  sbcimg  3211  sbcan  3212  sbcangOLD  3213  sbcor  3214  sbcorgOLD  3215  sbcbig  3216  sbcal  3220  sbcalgOLD  3221  sbcex2  3222  sbcexgOLD  3223  sbc3angOLD  3232  sbcel1v  3233  sbcel1gvOLD  3234  sbctt  3239  sbcralt  3249  sbcrexgOLD  3254  sbcreu  3255  sbcreugOLD  3256  rspsbc  3258  rspesbca  3260  sbcel12  3653  sbcel12gOLD  3654  sbceqg  3655  csbif  3807  csbifgOLD  3808  sbcbrg  4292  csbopabg  4314  opelopabsb  4500  onminex  4822  findes  4910  iota4  5471  csbiotag  5482  csbriotag  6598  nn0ind-raph  10408  uzind4s  10574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-11 1764  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-clab 2430  df-cleq 2436  df-clel 2439  df-sbc 3171
  Copyright terms: Public domain W3C validator