New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 3047 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 3049 instead of df-sbc 3047. (dfsbcq2 3049 is needed because
unlike Quine we do not overload the df-sb 1649 syntax.) As a consequence of
these theorems, we can derive sbc8g 3053, which is a weaker version of
df-sbc 3047 that leaves substitution undefined when A is a proper class.
However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3053, so we will allow direct use of df-sbc 3047 after theorem sbc2or 3054 below. 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 | ⊢ (A = B → ([̣A / x]̣φ ↔ [̣B / x]̣φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2413 | . 2 ⊢ (A = B → (A ∈ {x ∣ φ} ↔ B ∈ {x ∣ φ})) | |
2 | df-sbc 3047 | . 2 ⊢ ([̣A / x]̣φ ↔ A ∈ {x ∣ φ}) | |
3 | df-sbc 3047 | . 2 ⊢ ([̣B / x]̣φ ↔ B ∈ {x ∣ φ}) | |
4 | 1, 2, 3 | 3bitr4g 279 | 1 ⊢ (A = B → ([̣A / x]̣φ ↔ [̣B / x]̣φ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 = wceq 1642 ∈ wcel 1710 {cab 2339 [̣wsbc 3046 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-cleq 2346 df-clel 2349 df-sbc 3047 |
This theorem is referenced by: sbceq1d 3051 sbc8g 3053 spsbc 3058 sbcco 3068 sbcco2 3069 sbcie2g 3079 elrabsf 3084 eqsbc3 3085 csbeq1 3139 sbcnestgf 3183 sbcco3g 3191 cbvralcsf 3198 |
Copyright terms: Public domain | W3C validator |