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

Theorem dfsbcq2 2994
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 1630 and substitution for class variables df-sbc 2992. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2993. (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 2343 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2270 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 2992 . . 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 1623   [wsb 1629    e. wcel 1684   {cab 2269   [.wsbc 2991
This theorem is referenced by:  sbsbc  2995  sbc8g  2998  sbc2or  2999  sbceq1a  3001  sbc5  3015  sbcng  3031  sbcimg  3032  sbcan  3033  sbcang  3034  sbcor  3035  sbcorg  3036  sbcbig  3037  sbcal  3038  sbcalg  3039  sbcex2  3040  sbcexg  3041  sbc3ang  3049  sbcel1gv  3050  sbcel2gv  3051  sbctt  3053  sbcralt  3063  sbcralg  3065  sbcrexg  3066  sbcreug  3067  rspsbc  3069  rspesbca  3071  sbcel12g  3096  sbceqg  3097  csbifg  3593  sbcbrg  4072  csbopabg  4094  opelopabsb  4275  onminex  4598  findes  4686  iota4  5237  csbiotag  5248  csbriotag  6317  nn0ind-raph  10112  uzind4s  10278  iuninc  23158  measiuns  23544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-clab 2270  df-cleq 2276  df-clel 2279  df-sbc 2992
  Copyright terms: Public domain W3C validator