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

Theorem dfsbcq2 2996
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 1632 and substitution for class variables df-sbc 2994. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2995. (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 2345 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2272 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 2994 . . 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 1624   [wsb 1631    e. wcel 1685   {cab 2271   [.wsbc 2993
This theorem is referenced by:  sbsbc  2997  sbc8g  3000  sbc2or  3001  sbceq1a  3003  sbc5  3017  sbcng  3033  sbcimg  3034  sbcan  3035  sbcang  3036  sbcor  3037  sbcorg  3038  sbcbig  3039  sbcal  3040  sbcalg  3041  sbcex2  3042  sbcexg  3043  sbc3ang  3051  sbcel1gv  3052  sbcel2gv  3053  sbctt  3055  sbcralt  3065  sbcralg  3067  sbcrexg  3068  sbcreug  3069  rspsbc  3071  rspesbca  3073  sbcel12g  3098  sbceqg  3099  csbifg  3595  sbcbrg  4074  csbopabg  4096  opelopabsb  4275  onminex  4598  findes  4686  iota4  6271  csbriotag  6313  nn0ind-raph  10108  uzind4s  10274
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-clab 2272  df-cleq 2278  df-clel 2281  df-sbc 2994
  Copyright terms: Public domain W3C validator