Description: Bound-variable hypothesis builder for the at-most-one quantifier. See nfmod for a version without disjoint variable conditions but requiring ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) (Revised by BJ, 28-Jan-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfmodv.1 | |- F/ y ph |
|
| nfmodv.2 | |- ( ph -> F/ x ps ) |
||
| Assertion | nfmodv | |- ( ph -> F/ x E* y ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfmodv.1 | |- F/ y ph |
|
| 2 | nfmodv.2 | |- ( ph -> F/ x ps ) |
|
| 3 | df-mo | |- ( E* y ps <-> E. z A. y ( ps -> y = z ) ) |
|
| 4 | nfv | |- F/ z ph |
|
| 5 | nfvd | |- ( ph -> F/ x y = z ) |
|
| 6 | 2 5 | nfimd | |- ( ph -> F/ x ( ps -> y = z ) ) |
| 7 | 1 6 | nfald | |- ( ph -> F/ x A. y ( ps -> y = z ) ) |
| 8 | 4 7 | nfexd | |- ( ph -> F/ x E. z A. y ( ps -> y = z ) ) |
| 9 | 3 8 | nfxfrd | |- ( ph -> F/ x E* y ps ) |