![]() |
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 2963 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 2965 instead of df-sbc 2963. (dfsbcq2 2965 is needed because
unlike Quine we do not overload the df-sb 1763 syntax.) As a consequence of
these theorems, we can derive sbc8g 2970, which is a weaker version of
df-sbc 2963 that leaves substitution undefined when ![]() However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2970, so we will allow direct use of df-sbc 2963. 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 2240 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-sbc 2963 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-sbc 2963 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3bitr4g 223 |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 df-sbc 2963 |
This theorem is referenced by: sbceq1d 2967 sbc8g 2970 spsbc 2974 sbcco 2984 sbcco2 2985 sbcie2g 2996 elrabsf 3001 eqsbc1 3002 csbeq1 3060 sbcnestgf 3108 sbcco3g 3114 cbvralcsf 3119 cbvrexcsf 3120 findes 4598 ralrnmpt 5653 rexrnmpt 5654 findcard2 6882 findcard2s 6883 ac6sfi 6891 nn1suc 8914 uzind4s2 9567 indstr 9569 bezoutlemmain 11969 prmind2 12090 |
Copyright terms: Public domain | W3C validator |