Metamath Proof Explorer


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 )