![]() |
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 2327 and sbco2vv 2101. Usage of this theorem is discouraged because it depends on ax-13 2372. (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 2244 | . . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑧][𝑧 / 𝑥]𝜑)) | |
2 | sbequ 2087 | . . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | bitr3d 281 | . . 3 ⊢ (𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
4 | 3 | sps 2179 | . 2 ⊢ (∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
5 | nfnae 2434 | . . 3 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑦 | |
6 | sbco2.1 | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
7 | 6 | nfsb4 2500 | . . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
8 | 2 | a1i 11 | . . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))) |
9 | 5, 7, 8 | sbied 2503 | . 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
10 | 4, 9 | pm2.61i 182 | 1 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∀wal 1540 Ⅎwnf 1786 [wsb 2068 |
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 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 ax-13 2372 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 |
This theorem is referenced by: sbco2d 2512 sb7f 2525 cbvab 2809 clelsb2OLD 2863 clelsb1f 2909 sbcco 3804 |
Copyright terms: Public domain | W3C validator |