ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfsbcq2 Unicode version

Theorem dfsbcq2 2885
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 1721 and substitution for class variables df-sbc 2883. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2884. (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 2180 . 2  |-  ( y  =  A  ->  (
y  e.  { x  |  ph }  <->  A  e.  { x  |  ph }
) )
2 df-clab 2104 . 2  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
3 df-sbc 2883 . . 3  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
43bicomi 131 . 2  |-  ( A  e.  { x  | 
ph }  <->  [. A  /  x ]. ph )
51, 2, 43bitr3g 221 1  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1316    e. wcel 1465   [wsb 1720   {cab 2103   [.wsbc 2882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-clab 2104  df-cleq 2110  df-clel 2113  df-sbc 2883
This theorem is referenced by:  sbsbc  2886  sbc8g  2889  sbceq1a  2891  sbc5  2905  sbcng  2921  sbcimg  2922  sbcan  2923  sbcang  2924  sbcor  2925  sbcorg  2926  sbcbig  2927  sbcal  2932  sbcalg  2933  sbcex2  2934  sbcexg  2935  sbcel1v  2943  sbctt  2947  sbcralt  2957  sbcrext  2958  sbcralg  2959  sbcreug  2961  rspsbc  2963  rspesbca  2965  sbcel12g  2988  sbceqg  2989  sbcbrg  3952  csbopabg  3976  opelopabsb  4152  findes  4487  iota4  5076  csbiotag  5086  csbriotag  5710  nn0ind-raph  9136  uzind4s  9353  bezoutlemmain  11613  bezoutlemex  11616
  Copyright terms: Public domain W3C validator