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 y φ
nfald2.2 φ ¬ x x = y x ψ
Assertion nfexd2 φ x y ψ

Proof

Step Hyp Ref Expression
1 nfald2.1 y φ
2 nfald2.2 φ ¬ x x = y x ψ
3 df-ex y ψ ¬ y ¬ ψ
4 2 nfnd φ ¬ x x = y x ¬ ψ
5 1 4 nfald2 φ x y ¬ ψ
6 5 nfnd φ x ¬ y ¬ ψ
7 3 6 nfxfrd φ x y ψ