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

Theorem dfsbcq2 2938
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 1884 and substitution for class variables df-sbc 2936. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2937. (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 2316 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2243 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 2936 . . 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 6    <-> wb 178    = wceq 1619    e. wcel 1621   [wsb 1883   {cab 2242   [.wsbc 2935
This theorem is referenced by:  sbsbc  2939  sbc8g  2942  sbc2or  2943  sbceq1a  2945  sbc5  2959  sbcng  2975  sbcimg  2976  sbcan  2977  sbcang  2978  sbcor  2979  sbcorg  2980  sbcbig  2981  sbcal  2982  sbcalg  2983  sbcex2  2984  sbcexg  2985  sbc3ang  2993  sbcel1gv  2994  sbcel2gv  2995  sbctt  2997  sbcralt  3007  sbcralg  3009  sbcrexg  3010  sbcreug  3011  ra4sbc  3013  ra4esbca  3015  sbcel12g  3038  sbceqg  3039  csbifg  3534  sbcbrg  4012  csbopabg  4034  opelopabsb  4212  onminex  4535  findes  4623  iota4  6208  csbriotag  6250  nn0ind-raph  10044  uzind4s  10210
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-clab 2243  df-cleq 2249  df-clel 2252  df-sbc 2936
  Copyright terms: Public domain W3C validator