![]() |
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 3558 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 = wceq 1542 ∈ wcel 2107 Vcvv 3448 |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 |
This theorem is referenced by: morex 3682 al0ssb 5270 rext 5410 relop 5811 dfpo2 6253 frxp 8063 frxp2 8081 findcard 9114 pssnn 9119 ssfi 9124 pssnnOLD 9216 fiint 9275 marypha1lem 9376 dfom3 9590 elom3 9591 ttrclss 9663 aceq3lem 10063 dfac3 10064 dfac5lem4 10069 dfac8 10078 dfac9 10079 dfacacn 10084 dfac13 10085 kmlem1 10093 kmlem10 10102 fin23lem34 10289 fin23lem35 10290 zorn2lem7 10445 zornn0g 10448 axgroth6 10771 nnunb 12416 symggen 19259 gsumval3lem2 19690 gsumzaddlem 19705 dfac14 22985 i1fd 25061 chlimi 30218 zarclssn 32494 ddemeas 32875 dfon2lem4 34400 dfon2lem5 34401 dfon2lem7 34403 ttac 41389 dfac11 41418 dfac21 41422 setrec2fun 47211 |
Copyright terms: Public domain | W3C validator |