![]() |
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 3776 nalset 5313 dfpo2 6295 isowe2 7349 tfisi 7850 findcard2 9166 findcard2OLD 9286 marypha1lem 9430 setind 9731 karden 9892 kmlem4 10150 axgroth3 10828 ramcl 16964 alexsubALTlem3 23560 i1fd 25205 dfon2lem6 34835 trer 35293 bj-ru0 35915 eleq2w2ALT 36020 elsetrecslem 47828 |
Copyright terms: Public domain | W3C validator |