![]() |
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 2072 and rspsbc 3874. (Contributed by NM, 16-Jan-2004.) |
Ref | Expression |
---|---|
spsbc | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stdpc4 2072 | . . . 4 ⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | |
2 | sbsbc 3782 | . . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | |
3 | 1, 2 | sylib 217 | . . 3 ⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) |
4 | dfsbcq 3780 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
5 | 3, 4 | imbitrid 243 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)) |
6 | 5 | vtocleg 3546 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 = wceq 1542 [wsb 2068 ∈ wcel 2107 [wsbc 3778 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-sbc 3779 |
This theorem is referenced by: spsbcd 3792 sbcth 3793 sbcthdv 3794 sbceqalOLD 3845 sbcimdvOLD 3853 csbiebt 3924 csbexg 5311 pm14.18 43187 sbcbi 43300 onfrALTlem3 43305 sbc3orgVD 43612 sbcbiVD 43637 csbingVD 43645 onfrALTlem3VD 43648 csbeq2gVD 43653 csbunigVD 43659 |
Copyright terms: Public domain | W3C validator |