![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > spvv | Structured version Visualization version GIF version |
Description: Specialization, using implicit substitution. Version of spv 2392 with a disjoint variable condition, which does not require ax-7 2011, ax-12 2171, ax-13 2371. (Contributed by NM, 30-Aug-1993.) (Revised by BJ, 31-May-2019.) |
Ref | Expression |
---|---|
spvv.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spvv | ⊢ (∀𝑥𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spvv.1 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
2 | 1 | biimpd 228 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
3 | 2 | spimvw 1999 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 |
This theorem depends on definitions: df-bi 206 df-ex 1782 |
This theorem is referenced by: chvarvv 2002 nfcr 2888 ru 3775 nalset 5312 dfpo2 6292 isowe2 7343 tfisi 7844 findcard2 9160 findcard2OLD 9280 marypha1lem 9424 setind 9725 karden 9886 kmlem4 10144 axgroth3 10822 ramcl 16958 alexsubALTlem3 23544 i1fd 25189 dfon2lem6 34748 trer 35189 bj-ru0 35811 eleq2w2ALT 35916 elsetrecslem 47697 |
Copyright terms: Public domain | W3C validator |