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 2910 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 2912 instead of df-sbc 2910. (dfsbcq2 2912 is needed because
unlike Quine we do not overload the df-sb 1736 syntax.) As a consequence of
these theorems, we can derive sbc8g 2916, which is a weaker version of
df-sbc 2910 that leaves substitution undefined when is a proper class.
However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2916, so we will allow direct use of df-sbc 2910. 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 2202 | . 2 | |
2 | df-sbc 2910 | . 2 | |
3 | df-sbc 2910 | . 2 | |
4 | 1, 2, 3 | 3bitr4g 222 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1331 wcel 1480 cab 2125 wsbc 2909 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-clel 2135 df-sbc 2910 |
This theorem is referenced by: sbceq1d 2914 sbc8g 2916 spsbc 2920 sbcco 2930 sbcco2 2931 sbcie2g 2942 elrabsf 2947 eqsbc3 2948 csbeq1 3006 sbcnestgf 3051 sbcco3g 3057 cbvralcsf 3062 cbvrexcsf 3063 findes 4517 ralrnmpt 5562 rexrnmpt 5563 findcard2 6783 findcard2s 6784 ac6sfi 6792 nn1suc 8739 uzind4s2 9386 indstr 9388 bezoutlemmain 11686 prmind2 11801 |
Copyright terms: Public domain | W3C validator |