![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sb2 | GIF version |
Description: One direction of a simplified definition of substitution. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sb2 | ⊢ (∀x(x = y → φ) → [y / x]φ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-4 1397 | . 2 ⊢ (∀x(x = y → φ) → (x = y → φ)) | |
2 | equs4 1610 | . 2 ⊢ (∀x(x = y → φ) → ∃x(x = y ∧ φ)) | |
3 | df-sb 1643 | . 2 ⊢ ([y / x]φ ↔ ((x = y → φ) ∧ ∃x(x = y ∧ φ))) | |
4 | 1, 2, 3 | sylanbrc 394 | 1 ⊢ (∀x(x = y → φ) → [y / x]φ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∀wal 1240 ∃wex 1378 [wsb 1642 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-i9 1420 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 df-sb 1643 |
This theorem is referenced by: stdpc4 1655 equsb1 1665 equsb2 1666 sbiedh 1667 sb6f 1681 hbsb2a 1684 hbsb2e 1685 sbcof2 1688 sb3 1709 sb4b 1712 sb4bor 1713 hbsb2 1714 nfsb2or 1715 sb6rf 1730 sbi1v 1768 sbalyz 1872 iota4 4828 |
Copyright terms: Public domain | W3C validator |