![]() |
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 3586 | . 2 ⊢ (𝐴 ∈ V → (∀𝑥𝜑 → 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1538 = wceq 1540 ∈ wcel 2105 Vcvv 3473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 |
This theorem is referenced by: morex 3715 al0ssb 5308 rext 5448 relop 5850 dfpo2 6295 frxp 8117 frxp2 8135 findcard 9169 pssnn 9174 ssfi 9179 pssnnOLD 9271 fiint 9330 marypha1lem 9434 dfom3 9648 elom3 9649 ttrclss 9721 aceq3lem 10121 dfac3 10122 dfac5lem4 10127 dfac8 10136 dfac9 10137 dfacacn 10142 dfac13 10143 kmlem1 10151 kmlem10 10160 fin23lem34 10347 fin23lem35 10348 zorn2lem7 10503 zornn0g 10506 axgroth6 10829 nnunb 12475 symggen 19386 gsumval3lem2 19822 gsumzaddlem 19837 dfac14 23442 i1fd 25530 chlimi 30920 zarclssn 33317 ddemeas 33698 dfon2lem4 35228 dfon2lem5 35229 dfon2lem7 35231 ttac 42238 dfac11 42267 dfac21 42271 setrec2fun 47899 |
Copyright terms: Public domain | W3C validator |