Description: Variation on nfexd which adds the hypothesis that x and y are distinct in the inner subproof. Usage of this theorem is discouraged because it depends on ax-13 . Check out nfexd for a version requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfald2.1 | |- F/ y ph |
|
nfald2.2 | |- ( ( ph /\ -. A. x x = y ) -> F/ x ps ) |
||
Assertion | nfexd2 | |- ( ph -> F/ x E. y ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfald2.1 | |- F/ y ph |
|
2 | nfald2.2 | |- ( ( ph /\ -. A. x x = y ) -> F/ x ps ) |
|
3 | df-ex | |- ( E. y ps <-> -. A. y -. ps ) |
|
4 | 2 | nfnd | |- ( ( ph /\ -. A. x x = y ) -> F/ x -. ps ) |
5 | 1 4 | nfald2 | |- ( ph -> F/ x A. y -. ps ) |
6 | 5 | nfnd | |- ( ph -> F/ x -. A. y -. ps ) |
7 | 3 6 | nfxfrd | |- ( ph -> F/ x E. y ps ) |