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

Theorem dfsbcq2 2969
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 2967. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2968. (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 2318 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2245 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 2967 . . 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 2244   [.wsbc 2966
This theorem is referenced by:  sbsbc  2970  sbc8g  2973  sbc2or  2974  sbceq1a  2976  sbc5  2990  sbcng  3006  sbcimg  3007  sbcan  3008  sbcang  3009  sbcor  3010  sbcorg  3011  sbcbig  3012  sbcal  3013  sbcalg  3014  sbcex2  3015  sbcexg  3016  sbc3ang  3024  sbcel1gv  3025  sbcel2gv  3026  sbctt  3028  sbcralt  3038  sbcralg  3040  sbcrexg  3041  sbcreug  3042  ra4sbc  3044  ra4esbca  3046  sbcel12g  3071  sbceqg  3072  csbifg  3567  sbcbrg  4046  csbopabg  4068  opelopabsb  4247  onminex  4570  findes  4658  iota4  6243  csbriotag  6285  nn0ind-raph  10079  uzind4s  10245
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 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-clab 2245  df-cleq 2251  df-clel 2254  df-sbc 2967
  Copyright terms: Public domain W3C validator