![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > spv | Structured version Visualization version GIF version |
Description: Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
spv.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spv | ⊢ (∀𝑥𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spv.1 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
2 | 1 | biimpd 221 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
3 | 2 | spimv 2412 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∀wal 1656 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-12 2222 ax-13 2391 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1881 df-nf 1885 |
This theorem is referenced by: cbvalv 2427 ru 3662 nalset 5021 isowe2 6856 tfisi 7320 findcard2 8470 marypha1lem 8609 setind 8888 karden 9036 kmlem4 9291 axgroth3 9969 ramcl 16105 alexsubALTlem3 22224 i1fd 23848 dfpo2 32188 dfon2lem6 32232 trer 32850 axc11n-16 35014 elsetrecslem 43341 |
Copyright terms: Public domain | W3C validator |