![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dfsbcq | GIF 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 2964 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 2966 instead of df-sbc 2964. (dfsbcq2 2966 is needed because
unlike Quine we do not overload the df-sb 1763 syntax.) As a consequence of
these theorems, we can derive sbc8g 2971, which is a weaker version of
df-sbc 2964 that leaves substitution undefined when 𝐴 is a
proper class.
However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2971, so we will allow direct use of df-sbc 2964. 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 2964 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
3 | df-sbc 2964 | . 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}) | |
4 | 1, 2, 3 | 3bitr4g 223 | 1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 = wceq 1353 ∈ wcel 2148 {cab 2163 [wsbc 2963 |
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 2964 |
This theorem is referenced by: sbceq1d 2968 sbc8g 2971 spsbc 2975 sbcco 2985 sbcco2 2986 sbcie2g 2997 elrabsf 3002 eqsbc1 3003 csbeq1 3061 sbcnestgf 3109 sbcco3g 3115 cbvralcsf 3120 cbvrexcsf 3121 findes 4603 ralrnmpt 5659 rexrnmpt 5660 findcard2 6889 findcard2s 6890 ac6sfi 6898 nn1suc 8938 uzind4s2 9591 indstr 9593 bezoutlemmain 11999 prmind2 12120 |
Copyright terms: Public domain | W3C validator |