\fo\and分配
theorem fo_and_dist {x: set} (A B: wff x):
$ \fo x (A \and B) \iff \fo x A \and \fo x B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | (\fo x (A \and B) \imp \fo x A \and \fo x B) \imp (\fo x A \and \fo x B \imp \fo x (A \and B)) \imp (\fo x (A \and B) \iff \fo x A \and \fo x B) |
|
| 2 | imp_collectr_and | (\fo x (A \and B) \imp \fo x A) \imp (\fo x (A \and B) \imp \fo x B) \imp \fo x (A \and B) \imp \fo x A \and \fo x B |
|
| 3 | and_splitl | A \and B \imp A |
|
| 4 | 3 | imp_intro_fo | \fo x (A \and B) \imp \fo x A |
| 5 | 2, 4 | ax_mp | (\fo x (A \and B) \imp \fo x B) \imp \fo x (A \and B) \imp \fo x A \and \fo x B |
| 6 | and_splitr | A \and B \imp B |
|
| 7 | 6 | imp_intro_fo | \fo x (A \and B) \imp \fo x B |
| 8 | 5, 7 | ax_mp | \fo x (A \and B) \imp \fo x A \and \fo x B |
| 9 | 1, 8 | ax_mp | (\fo x A \and \fo x B \imp \fo x (A \and B)) \imp (\fo x (A \and B) \iff \fo x A \and \fo x B) |
| 10 | imp_nested_assemb_and | (\fo x A \imp \fo x B \imp \fo x (A \and B)) \imp \fo x A \and \fo x B \imp \fo x (A \and B) |
|
| 11 | imp_introl_imp | (\fo x (B \imp A \and B) \imp \fo x B \imp \fo x (A \and B)) \imp (\fo x A \imp \fo x (B \imp A \and B)) \imp \fo x A \imp \fo x B \imp \fo x (A \and B) |
|
| 12 | fo_imp_ins | \fo x (B \imp A \and B) \imp \fo x B \imp \fo x (A \and B) |
|
| 13 | 11, 12 | ax_mp | (\fo x A \imp \fo x (B \imp A \and B)) \imp \fo x A \imp \fo x B \imp \fo x (A \and B) |
| 14 | and_comp | A \imp B \imp A \and B |
|
| 15 | 14 | imp_intro_fo | \fo x A \imp \fo x (B \imp A \and B) |
| 16 | 13, 15 | ax_mp | \fo x A \imp \fo x B \imp \fo x (A \and B) |
| 17 | 10, 16 | ax_mp | \fo x A \and \fo x B \imp \fo x (A \and B) |
| 18 | 9, 17 | ax_mp | \fo x (A \and B) \iff \fo x A \and \fo x B |