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

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

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2100 . 2
2 df-clab 2027 . 2
3 df-sbc 2765 . . 3
43bicomi 123 . 2
51, 2, 43bitr3g 211 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 98   wceq 1243   wcel 1393  wsb 1645  cab 2026  wsbc 2764 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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-clab 2027  df-cleq 2033  df-clel 2036  df-sbc 2765 This theorem is referenced by:  sbsbc  2768  sbc8g  2771  sbceq1a  2773  sbc5  2787  sbcng  2803  sbcimg  2804  sbcan  2805  sbcang  2806  sbcor  2807  sbcorg  2808  sbcbig  2809  sbcal  2810  sbcalg  2811  sbcex2  2812  sbcexg  2813  sbc3ang  2820  sbcel1gv  2821  sbctt  2824  sbcralt  2834  sbcrext  2835  sbcralg  2836  sbcreug  2838  rspsbc  2840  rspesbca  2842  sbcel12g  2865  sbceqg  2866  sbcbrg  3813  csbopabg  3835  opelopabsb  3997  findes  4326  iota4  4885  csbiotag  4895  csbriotag  5480  nn0ind-raph  8355  uzind4s  8533
 Copyright terms: Public domain W3C validator