Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sb6 | GIF version |
Description: Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.) |
Ref | Expression |
---|---|
sb6 | ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sb56 1872 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | |
2 | 1 | anbi2i 453 | . 2 ⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
3 | df-sb 1750 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | |
4 | ax-4 1497 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜑)) | |
5 | 4 | pm4.71ri 390 | . 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
6 | 2, 3, 5 | 3bitr4i 211 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1340 ∃wex 1479 [wsb 1749 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 |
This theorem depends on definitions: df-bi 116 df-sb 1750 |
This theorem is referenced by: sb5 1874 sbnv 1875 sbanv 1876 sbi1v 1878 sbi2v 1879 hbs1 1925 2sb6 1971 sbcom2v 1972 sb6a 1975 sb7af 1980 sbalyz 1986 sbal1yz 1988 exsb 1995 sbal2 2007 cbvabw 2287 nfabdw 2325 csbcow 3051 |
Copyright terms: Public domain | W3C validator |