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

Theorem dfsbcq2 2740
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 1624 and substitution for class variables df-sbc 2738. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2739. (Contributed by NM, 31-Dec-2016.)
Assertion
Ref Expression
dfsbcq2  [.  ].

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2078 . 2  {  |  }  {  |  }
2 df-clab 2005 . 2  {  |  }
3 df-sbc 2738 . . 3  [.  ].  {  |  }
43bicomi 123 . 2  {  |  }  [.  ].
51, 2, 43bitr3g 211 1  [.  ].
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98   wceq 1226   wcel 1370  wsb 1623   {cab 2004   [.wsbc 2737
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-17 1396  ax-ial 1405  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-clab 2005  df-cleq 2011  df-clel 2014  df-sbc 2738
This theorem is referenced by:  sbsbc  2741  sbc8g  2744  sbceq1a  2746  sbc5  2760  sbcng  2776  sbcimg  2777  sbcan  2778  sbcang  2779  sbcor  2780  sbcorg  2781  sbcbig  2782  sbcal  2783  sbcalg  2784  sbcex2  2785  sbcexg  2786  sbc3ang  2793  sbcel1gv  2794  sbctt  2797  sbcralt  2807  sbcrext  2808  sbcralg  2809  sbcrexg  2810  sbcreug  2811  rspsbc  2813  rspesbca  2815  sbcel12g  2838  sbceqg  2839  sbcbrg  3783  csbopabg  3805  opelopabsb  3967  findes  4249  iota4  4808  csbiotag  4818  csbriotag  5400
  Copyright terms: Public domain W3C validator