Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > spcv | Structured version Visualization version Unicode version |
Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.) |
Ref | Expression |
---|---|
spcv.1 | |
spcv.2 |
Ref | Expression |
---|---|
spcv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spcv.1 | . 2 | |
2 | spcv.2 | . . 3 | |
3 | 2 | spcgv 3293 | . 2 |
4 | 1, 3 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wal 1481 wceq 1483 wcel 1990 cvv 3200 |
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-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 |
This theorem is referenced by: morex 3390 rext 4916 relop 5272 frxp 7287 pssnn 8178 findcard 8199 fiint 8237 marypha1lem 8339 dfom3 8544 elom3 8545 aceq3lem 8943 dfac3 8944 dfac5lem4 8949 dfac8 8957 dfac9 8958 dfacacn 8963 dfac13 8964 kmlem1 8972 kmlem10 8981 fin23lem34 9168 fin23lem35 9169 zorn2lem7 9324 zornn0g 9327 axgroth6 9650 nnunb 11288 symggen 17890 gsumval3lem2 18307 gsumzaddlem 18321 dfac14 21421 i1fd 23448 chlimi 28091 ddemeas 30299 dfpo2 31645 dfon2lem4 31691 dfon2lem5 31692 dfon2lem7 31694 ttac 37603 dfac11 37632 dfac21 37636 setrec2fun 42439 |
Copyright terms: Public domain | W3C validator |