Description: Formula-building rule for the at-most-one quantifier (inference form). (Contributed by NM, 9-Mar-1995) (Revised by Mario Carneiro, 17-Oct-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mobii.1 | |- ( ps <-> ch ) |
|
| Assertion | mobii | |- ( E* x ps <-> E* x ch ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mobii.1 | |- ( ps <-> ch ) |
|
| 2 | mobi | |- ( A. x ( ps <-> ch ) -> ( E* x ps <-> E* x ch ) ) |
|
| 3 | 2 1 | mpg | |- ( E* x ps <-> E* x ch ) |