![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dfsbcq2 | Unicode version |
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 1774 and substitution for class variables df-sbc 2978. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2979. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2252 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-clab 2176 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-sbc 2978 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | bicomi 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 4 | 3bitr3g 222 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-clab 2176 df-cleq 2182 df-clel 2185 df-sbc 2978 |
This theorem is referenced by: sbsbc 2981 sbc8g 2985 sbceq1a 2987 sbc5 3001 sbcng 3018 sbcimg 3019 sbcan 3020 sbcang 3021 sbcor 3022 sbcorg 3023 sbcbig 3024 sbcal 3029 sbcalg 3030 sbcex2 3031 sbcexg 3032 sbcel1v 3040 sbctt 3044 sbcralt 3054 sbcrext 3055 sbcralg 3056 sbcreug 3058 rspsbc 3060 rspesbca 3062 sbcel12g 3087 sbceqg 3088 sbcbrg 4075 csbopabg 4099 opelopabsb 4281 findes 4623 iota4 5218 csbiotag 5231 csbriotag 5868 nn0ind-raph 9405 uzind4s 9626 bezoutlemmain 12040 bezoutlemex 12043 |
Copyright terms: Public domain | W3C validator |