Description: Bound-variable hypothesis builder for the at-most-one quantifier. (Contributed by NM, 8-Mar-1995) (Revised by Mario Carneiro, 7-Oct-2016) Adapt to new definition. (Revised by BJ, 1-Oct-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfmo1 | |- F/ x E* x ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-mo | |- ( E* x ph <-> E. y A. x ( ph -> x = y ) ) |
|
| 2 | nfa1 | |- F/ x A. x ( ph -> x = y ) |
|
| 3 | 2 | nfex | |- F/ x E. y A. x ( ph -> x = y ) |
| 4 | 1 3 | nfxfr | |- F/ x E* x ph |