| 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 2398 with a disjoint variable condition, which does not require ax-7 2007, ax-12 2177, ax-13 2377. (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 229 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
| 3 | 2 | spimvw 1995 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: chvarvv 1998 ru0 2127 nfcr 2895 ruOLD 3787 nalset 5313 dfpo2 6316 isowe2 7370 tfisi 7880 findcard2 9204 marypha1lem 9473 setind 9774 karden 9935 kmlem4 10194 axgroth3 10871 ramcl 17067 cnsubrglem 21434 alexsubALTlem3 24057 i1fd 25716 dfon2lem6 35789 trer 36317 eleq2w2ALT 37048 modelaxreplem1 44995 elsetrecslem 49218 |
| Copyright terms: Public domain | W3C validator |