Theorem nfexd2

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 )

Proof

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 )