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) Avoid ax-5 . (Revised by Wolf Lammen, 24-Sep-2023)
| 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 | 1 | biimpri | |- ( ch -> ps ) |
| 3 | 2 | moimi | |- ( E* x ps -> E* x ch ) |
| 4 | 1 | biimpi | |- ( ps -> ch ) |
| 5 | 4 | moimi | |- ( E* x ch -> E* x ps ) |
| 6 | 3 5 | impbii | |- ( E* x ps <-> E* x ch ) |