Description: Bound-variable hypothesis builder for the at-most-one quantifier. Deduction version of nfmo . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfmodv when possible. (Contributed by Mario Carneiro, 14-Nov-2016) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfmod.1 | |- F/ y ph |
|
| nfmod.2 | |- ( ph -> F/ x ps ) |
||
| Assertion | nfmod | |- ( ph -> F/ x E* y ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfmod.1 | |- F/ y ph |
|
| 2 | nfmod.2 | |- ( ph -> F/ x ps ) |
|
| 3 | 2 | adantr | |- ( ( ph /\ -. A. x x = y ) -> F/ x ps ) |
| 4 | 1 3 | nfmod2 | |- ( ph -> F/ x E* y ps ) |