![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbco2 | Structured version Visualization version GIF version |
Description: A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v 2342 and sbco2vv 2106. Usage of this theorem is discouraged because it depends on ax-13 2380. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Sep-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
sbco2.1 | ⊢ Ⅎ𝑧𝜑 |
Ref | Expression |
---|---|
sbco2 | ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbequ12 2251 | . . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑧][𝑧 / 𝑥]𝜑)) | |
2 | sbequ 2089 | . . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | bitr3d 284 | . . 3 ⊢ (𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
4 | 3 | sps 2183 | . 2 ⊢ (∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
5 | nfnae 2446 | . . 3 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑦 | |
6 | sbco2.1 | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
7 | 6 | nfsb4 2519 | . . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
8 | 2 | a1i 11 | . . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))) |
9 | 5, 7, 8 | sbied 2523 | . 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
10 | 4, 9 | pm2.61i 185 | 1 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∀wal 1537 Ⅎwnf 1786 [wsb 2070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-10 2143 ax-11 2159 ax-12 2176 ax-13 2380 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2071 |
This theorem is referenced by: sbco2d 2532 sb7f 2546 cbvab 2830 clelsb3f 2922 sbcco 3719 |
Copyright terms: Public domain | W3C validator |