![]() |
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 2341 and sbco2vv 2105. Usage of this theorem is discouraged because it depends on ax-13 2379. (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 2250 | . . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑧][𝑧 / 𝑥]𝜑)) | |
2 | sbequ 2088 | . . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | bitr3d 284 | . . 3 ⊢ (𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
4 | 3 | sps 2182 | . 2 ⊢ (∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
5 | nfnae 2445 | . . 3 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑦 | |
6 | sbco2.1 | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
7 | 6 | nfsb4 2518 | . . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
8 | 2 | a1i 11 | . . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))) |
9 | 5, 7, 8 | sbied 2522 | . 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
10 | 4, 9 | pm2.61i 185 | 1 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∀wal 1536 Ⅎwnf 1785 [wsb 2069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2142 ax-11 2158 ax-12 2175 ax-13 2379 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 |
This theorem is referenced by: sbco2d 2531 sb7f 2545 cbvab 2869 clelsb3f 2960 sbcco 3746 |
Copyright terms: Public domain | W3C validator |