Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dfsbcq | 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, provides us with a weak definition
of the proper substitution of a class for a set. Since our df-sbc 2883 does
not result in the same behavior as Quine's for proper classes, if we
wished to avoid conflict with Quine's definition we could start with this
theorem and dfsbcq2 2885 instead of df-sbc 2883. (dfsbcq2 2885 is needed because
unlike Quine we do not overload the df-sb 1721 syntax.) As a consequence of
these theorems, we can derive sbc8g 2889, which is a weaker version of
df-sbc 2883 that leaves substitution undefined when is a proper class.
However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2889, so we will allow direct use of df-sbc 2883. Proper substiution with a proper class is rarely needed, and when it is, we can simply use the expansion of Quine's definition. (Contributed by NM, 14-Apr-1995.) |
Ref | Expression |
---|---|
dfsbcq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2180 | . 2 | |
2 | df-sbc 2883 | . 2 | |
3 | df-sbc 2883 | . 2 | |
4 | 1, 2, 3 | 3bitr4g 222 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1316 wcel 1465 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-cleq 2110 df-clel 2113 df-sbc 2883 |
This theorem is referenced by: sbceq1d 2887 sbc8g 2889 spsbc 2893 sbcco 2903 sbcco2 2904 sbcie2g 2914 elrabsf 2919 eqsbc3 2920 csbeq1 2978 sbcnestgf 3021 sbcco3g 3027 cbvralcsf 3032 cbvrexcsf 3033 findes 4487 ralrnmpt 5530 rexrnmpt 5531 findcard2 6751 findcard2s 6752 ac6sfi 6760 nn1suc 8703 uzind4s2 9342 indstr 9344 bezoutlemmain 11598 prmind2 11713 |
Copyright terms: Public domain | W3C validator |