Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > spsbc | Structured version Visualization version GIF version |
Description: Specialization: if a formula is true for all sets, it is true for any class which is a set. Similar to Theorem 6.11 of [Quine] p. 44. This is Frege's ninth axiom per Proposition 58 of [Frege1879] p. 51. See also stdpc4 2353 and rspsbc 3518. (Contributed by NM, 16-Jan-2004.) |
Ref | Expression |
---|---|
spsbc | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stdpc4 2353 | . . . 4 ⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | |
2 | sbsbc 3439 | . . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | |
3 | 1, 2 | sylib 208 | . . 3 ⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) |
4 | dfsbcq 3437 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
5 | 3, 4 | syl5ib 234 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)) |
6 | 5 | vtocleg 3279 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1481 = wceq 1483 [wsb 1880 ∈ wcel 1990 [wsbc 3435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-tru 1486 df-ex 1705 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 df-sbc 3436 |
This theorem is referenced by: spsbcd 3449 sbcth 3450 sbcthdv 3451 sbceqal 3487 sbcimdv 3498 sbcimdvOLD 3499 csbiebt 3553 csbexg 4792 pm14.18 38629 sbcbi 38749 onfrALTlem3 38759 csbeq2gOLD 38765 sbc3orgVD 39086 sbcbiVD 39112 csbingVD 39120 onfrALTlem3VD 39123 csbeq2gVD 39128 csbunigVD 39134 |
Copyright terms: Public domain | W3C validator |