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 2341 and rspsbc 3484. (Contributed by NM, 16-Jan-2004.) |
Ref | Expression |
---|---|
spsbc | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stdpc4 2341 | . . . 4 ⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | |
2 | sbsbc 3406 | . . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | |
3 | 1, 2 | sylib 207 | . . 3 ⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) |
4 | dfsbcq 3404 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
5 | 3, 4 | syl5ib 233 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)) |
6 | 5 | vtocleg 3252 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 = wceq 1475 [wsb 1867 ∈ wcel 1977 [wsbc 3402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-tru 1478 df-ex 1696 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 df-sbc 3403 |
This theorem is referenced by: spsbcd 3416 sbcth 3417 sbcthdv 3418 sbceqal 3454 sbcimdv 3465 sbcimdvOLD 3466 csbiebt 3519 csbexg 4720 pm14.18 37651 sbcbi 37770 onfrALTlem3 37780 csbeq2gOLD 37786 sbc3orgVD 38108 sbcbiVD 38134 csbingVD 38142 onfrALTlem3VD 38145 csbeq2gVD 38150 csbunigVD 38156 |
Copyright terms: Public domain | W3C validator |