Description: Bound-variable hypothesis builder for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 . See nfmodv for a version replacing the distinctor with a disjoint variable condition, not requiring ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) Avoid df-eu . (Revised by BJ, 14-Oct-2022) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfmod2.1 | |- F/ y ph |
|
| nfmod2.2 | |- ( ( ph /\ -. A. x x = y ) -> F/ x ps ) |
||
| Assertion | nfmod2 | |- ( ph -> F/ x E* y ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfmod2.1 | |- F/ y ph |
|
| 2 | nfmod2.2 | |- ( ( ph /\ -. A. x x = y ) -> F/ x ps ) |
|
| 3 | df-mo | |- ( E* y ps <-> E. z A. y ( ps -> y = z ) ) |
|
| 4 | nfv | |- F/ z ph |
|
| 5 | nfeqf1 | |- ( -. A. x x = y -> F/ x y = z ) |
|
| 6 | 5 | adantl | |- ( ( ph /\ -. A. x x = y ) -> F/ x y = z ) |
| 7 | 2 6 | nfimd | |- ( ( ph /\ -. A. x x = y ) -> F/ x ( ps -> y = z ) ) |
| 8 | 1 7 | nfald2 | |- ( ph -> F/ x A. y ( ps -> y = z ) ) |
| 9 | 4 8 | nfexd | |- ( ph -> F/ x E. z A. y ( ps -> y = z ) ) |
| 10 | 3 9 | nfxfrd | |- ( ph -> F/ x E* y ps ) |