![]() |
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 | ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-4 1510 | . 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜑)) | |
2 | equs4 1725 | . 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
3 | df-sb 1763 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | |
4 | 1, 2, 3 | sylanbrc 417 | 1 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∀wal 1351 ∃wex 1492 [wsb 1762 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-i9 1530 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-sb 1763 |
This theorem is referenced by: stdpc4 1775 equsb1 1785 equsb2 1786 sbiedh 1787 sb6f 1803 hbsb2a 1806 hbsb2e 1807 sbcof2 1810 sb3 1831 sb4b 1834 sb4bor 1835 hbsb2 1836 nfsb2or 1837 sb6rf 1853 sbi1v 1891 sbalyz 1999 iota4 5192 |
Copyright terms: Public domain | W3C validator |