替换操作对蕴涵的插入律。
theorem sb_imp_ins {x: set} (y: set) (A B: wff x):
$ \sb y x (A \imp B) \imp \sb y x A \imp \sb y x B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | (\fo t (t = y \imp \fo x (x = t \imp A \imp B)) \imp \fo t ((t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B))) \imp
(\fo t ((t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B)) \imp
\fo t (t = y \imp \fo x (x = t \imp A)) \imp
\fo t (t = y \imp \fo x (x = t \imp B))) \imp
\fo t (t = y \imp \fo x (x = t \imp A \imp B)) \imp
\fo t (t = y \imp \fo x (x = t \imp A)) \imp
\fo t (t = y \imp \fo x (x = t \imp B)) |
|
| 2 | imp_tran | ((t = y \imp \fo x (x = t \imp A \imp B)) \imp t = y \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B)) \imp ((t = y \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B)) \imp (t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B)) \imp (t = y \imp \fo x (x = t \imp A \imp B)) \imp (t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B) |
|
| 3 | imp_introl_imp | (\fo x (x = t \imp A \imp B) \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B)) \imp (t = y \imp \fo x (x = t \imp A \imp B)) \imp t = y \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B) |
|
| 4 | imp_tran | (\fo x (x = t \imp A \imp B) \imp \fo x ((x = t \imp A) \imp x = t \imp B)) \imp (\fo x ((x = t \imp A) \imp x = t \imp B) \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B)) \imp \fo x (x = t \imp A \imp B) \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B) |
|
| 5 | imp_imp_insl | (x = t \imp A \imp B) \imp (x = t \imp A) \imp x = t \imp B |
|
| 6 | 5 | imp_intro_fo | \fo x (x = t \imp A \imp B) \imp \fo x ((x = t \imp A) \imp x = t \imp B) |
| 7 | 4, 6 | ax_mp | (\fo x ((x = t \imp A) \imp x = t \imp B) \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B)) \imp \fo x (x = t \imp A \imp B) \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B) |
| 8 | fo_imp_ins | \fo x ((x = t \imp A) \imp x = t \imp B) \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B) |
|
| 9 | 7, 8 | ax_mp | \fo x (x = t \imp A \imp B) \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B) |
| 10 | 3, 9 | ax_mp | (t = y \imp \fo x (x = t \imp A \imp B)) \imp t = y \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B) |
| 11 | 2, 10 | ax_mp | ((t = y \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B)) \imp (t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B)) \imp (t = y \imp \fo x (x = t \imp A \imp B)) \imp (t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B) |
| 12 | imp_imp_insl | (t = y \imp \fo x (x = t \imp A) \imp \fo x (x = t \imp B)) \imp (t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B) |
|
| 13 | 11, 12 | ax_mp | (t = y \imp \fo x (x = t \imp A \imp B)) \imp (t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B) |
| 14 | 13 | imp_intro_fo | \fo t (t = y \imp \fo x (x = t \imp A \imp B)) \imp \fo t ((t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B)) |
| 15 | 1, 14 | ax_mp | (\fo t ((t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B)) \imp
\fo t (t = y \imp \fo x (x = t \imp A)) \imp
\fo t (t = y \imp \fo x (x = t \imp B))) \imp
\fo t (t = y \imp \fo x (x = t \imp A \imp B)) \imp
\fo t (t = y \imp \fo x (x = t \imp A)) \imp
\fo t (t = y \imp \fo x (x = t \imp B)) |
| 16 | fo_imp_ins | \fo t ((t = y \imp \fo x (x = t \imp A)) \imp t = y \imp \fo x (x = t \imp B)) \imp \fo t (t = y \imp \fo x (x = t \imp A)) \imp \fo t (t = y \imp \fo x (x = t \imp B)) |
|
| 17 | 15, 16 | ax_mp | \fo t (t = y \imp \fo x (x = t \imp A \imp B)) \imp \fo t (t = y \imp \fo x (x = t \imp A)) \imp \fo t (t = y \imp \fo x (x = t \imp B)) |
| 18 | 17 | conv sb | \sb y x (A \imp B) \imp \sb y x A \imp \sb y x B |