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 2947 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 2949 instead of df-sbc 2947. (dfsbcq2 2949 is needed because
unlike Quine we do not overload the df-sb 1750 syntax.) As a consequence of
these theorems, we can derive sbc8g 2953, which is a weaker version of
df-sbc 2947 that leaves substitution undefined when is a proper class.
However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2953, so we will allow direct use of df-sbc 2947. 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 2227 | . 2 | |
2 | df-sbc 2947 | . 2 | |
3 | df-sbc 2947 | . 2 | |
4 | 1, 2, 3 | 3bitr4g 222 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1342 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-cleq 2157 df-clel 2160 df-sbc 2947 |
This theorem is referenced by: sbceq1d 2951 sbc8g 2953 spsbc 2957 sbcco 2967 sbcco2 2968 sbcie2g 2979 elrabsf 2984 eqsbc3 2985 csbeq1 3043 sbcnestgf 3091 sbcco3g 3097 cbvralcsf 3102 cbvrexcsf 3103 findes 4574 ralrnmpt 5621 rexrnmpt 5622 findcard2 6846 findcard2s 6847 ac6sfi 6855 nn1suc 8867 uzind4s2 9520 indstr 9522 bezoutlemmain 11916 prmind2 12031 |
Copyright terms: Public domain | W3C validator |