全称量词可以通过代入实例消去。
theorem fo_elim_sb {x: set} (y: set) (A: wff x): $ \fo x A \imp \sb y x A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | _nf_abs | \nf t \fo x A |
|
| 2 | imp_introrsl_imp | (\fo x A \imp \fo x (x = t \imp A)) \imp \fo x A \imp t = y \imp \fo x (x = t \imp A) |
|
| 3 | introl_imp | A \imp x = t \imp A |
|
| 4 | 3 | imp_intro_fo | \fo x A \imp \fo x (x = t \imp A) |
| 5 | 2, 4 | ax_mp | \fo x A \imp t = y \imp \fo x (x = t \imp A) |
| 6 | 1, 5 | imp_intrors_fo_nfls | \fo x A \imp \fo t (t = y \imp \fo x (x = t \imp A)) |
| 7 | 6 | conv sb | \fo x A \imp \sb y x A |