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 3592 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1526 = wceq 1528 ∈ wcel 2105 Vcvv 3492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-v 3494 |
This theorem is referenced by: morex 3707 al0ssb 5203 rext 5331 relop 5714 frxp 7809 pssnn 8724 findcard 8745 fiint 8783 marypha1lem 8885 dfom3 9098 elom3 9099 aceq3lem 9534 dfac3 9535 dfac5lem4 9540 dfac8 9549 dfac9 9550 dfacacn 9555 dfac13 9556 kmlem1 9564 kmlem10 9573 fin23lem34 9756 fin23lem35 9757 zorn2lem7 9912 zornn0g 9915 axgroth6 10238 nnunb 11881 symggen 18527 gsumval3lem2 18955 gsumzaddlem 18970 dfac14 22154 i1fd 24209 chlimi 28938 ddemeas 31394 dfpo2 32888 dfon2lem4 32928 dfon2lem5 32929 dfon2lem7 32931 ttac 39511 dfac11 39540 dfac21 39544 setrec2fun 44723 |
Copyright terms: Public domain | W3C validator |