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 2905 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 2907 instead of df-sbc 2905. (dfsbcq2 2907 is needed because
unlike Quine we do not overload the df-sb 1736 syntax.) As a consequence of
these theorems, we can derive sbc8g 2911, which is a weaker version of
df-sbc 2905 that leaves substitution undefined when 𝐴 is a
proper class.
However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2911, so we will allow direct use of df-sbc 2905. 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 2200 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-sbc 2905 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
3 | df-sbc 2905 | . 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 2123 [wsbc 2904 |
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 2119 |
This theorem depends on definitions: df-bi 116 df-cleq 2130 df-clel 2133 df-sbc 2905 |
This theorem is referenced by: sbceq1d 2909 sbc8g 2911 spsbc 2915 sbcco 2925 sbcco2 2926 sbcie2g 2937 elrabsf 2942 eqsbc3 2943 csbeq1 3001 sbcnestgf 3046 sbcco3g 3052 cbvralcsf 3057 cbvrexcsf 3058 findes 4512 ralrnmpt 5555 rexrnmpt 5556 findcard2 6776 findcard2s 6777 ac6sfi 6785 nn1suc 8732 uzind4s2 9379 indstr 9381 bezoutlemmain 11675 prmind2 11790 |
Copyright terms: Public domain | W3C validator |