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 1750 and substitution for class variables df-sbc 2947. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2948. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2227 | . 2 | |
2 | df-clab 2151 | . 2 | |
3 | df-sbc 2947 | . . 3 | |
4 | 3 | bicomi 131 | . 2 |
5 | 1, 2, 4 | 3bitr3g 221 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1342 wsb 1749 wcel 2135 cab 2150 wsbc 2946 |
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 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-clab 2151 df-cleq 2157 df-clel 2160 df-sbc 2947 |
This theorem is referenced by: sbsbc 2950 sbc8g 2953 sbceq1a 2955 sbc5 2969 sbcng 2986 sbcimg 2987 sbcan 2988 sbcang 2989 sbcor 2990 sbcorg 2991 sbcbig 2992 sbcal 2997 sbcalg 2998 sbcex2 2999 sbcexg 3000 sbcel1v 3008 sbctt 3012 sbcralt 3022 sbcrext 3023 sbcralg 3024 sbcreug 3026 rspsbc 3028 rspesbca 3030 sbcel12g 3055 sbceqg 3056 sbcbrg 4030 csbopabg 4054 opelopabsb 4232 findes 4574 iota4 5165 csbiotag 5175 csbriotag 5804 nn0ind-raph 9299 uzind4s 9519 bezoutlemmain 11916 bezoutlemex 11919 |
Copyright terms: Public domain | W3C validator |