![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > spcv | Structured version Visualization version GIF version |
Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.) |
Ref | Expression |
---|---|
spcv.1 | ⊢ 𝐴 ∈ V |
spcv.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcv | ⊢ (∀𝑥𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spcv.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | spcv.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | spcgv 3494 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∀wal 1599 = wceq 1601 ∈ wcel 2106 Vcvv 3397 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-v 3399 |
This theorem is referenced by: morex 3601 al0ssb 5027 rext 5148 relop 5518 frxp 7568 pssnn 8466 findcard 8487 fiint 8525 marypha1lem 8627 dfom3 8841 elom3 8842 aceq3lem 9276 dfac3 9277 dfac5lem4 9282 dfac8 9292 dfac9 9293 dfacacn 9298 dfac13 9299 kmlem1 9307 kmlem10 9316 fin23lem34 9503 fin23lem35 9504 zorn2lem7 9659 zornn0g 9662 axgroth6 9985 nnunb 11638 symggen 18273 gsumval3lem2 18693 gsumzaddlem 18707 dfac14 21830 i1fd 23885 chlimi 28663 ddemeas 30897 dfpo2 32239 dfon2lem4 32279 dfon2lem5 32280 dfon2lem7 32282 ttac 38544 dfac11 38573 dfac21 38577 setrec2fun 43526 |
Copyright terms: Public domain | W3C validator |