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 2956 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 2958 instead of df-sbc 2956. (dfsbcq2 2958 is needed because
unlike Quine we do not overload the df-sb 1756 syntax.) As a consequence of
these theorems, we can derive sbc8g 2962, which is a weaker version of
df-sbc 2956 that leaves substitution undefined when 𝐴 is a
proper class.
However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2962, so we will allow direct use of df-sbc 2956. 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 2233 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-sbc 2956 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
3 | df-sbc 2956 | . 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}) | |
4 | 1, 2, 3 | 3bitr4g 222 | 1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1348 ∈ wcel 2141 {cab 2156 [wsbc 2955 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-clel 2166 df-sbc 2956 |
This theorem is referenced by: sbceq1d 2960 sbc8g 2962 spsbc 2966 sbcco 2976 sbcco2 2977 sbcie2g 2988 elrabsf 2993 eqsbc1 2994 csbeq1 3052 sbcnestgf 3100 sbcco3g 3106 cbvralcsf 3111 cbvrexcsf 3112 findes 4587 ralrnmpt 5638 rexrnmpt 5639 findcard2 6867 findcard2s 6868 ac6sfi 6876 nn1suc 8897 uzind4s2 9550 indstr 9552 bezoutlemmain 11953 prmind2 12074 |
Copyright terms: Public domain | W3C validator |