Theorem nfald2

Description: Variation on nfald which adds the hypothesis that x and y are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016) Usage of this theorem is discouraged because it depends on ax-13 . Use nfald instead. (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfald2.1	|- F/ y ph
	nfald2.2	|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
Assertion	nfald2	|- ( ph -> F/ x A. 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		nfnae	|- F/ y -. A. x x = y
4	1 3	nfan	|- F/ y ( ph /\ -. A. x x = y )
5	4 2	nfald	|- ( ( ph /\ -. A. x x = y ) -> F/ x A. y ps )
6	5	ex	|- ( ph -> ( -. A. x x = y -> F/ x A. y ps ) )
7		nfa1	|- F/ y A. y ps
8		biidd	|- ( A. x x = y -> ( A. y ps <-> A. y ps ) )
9	8	drnf1	|- ( A. x x = y -> ( F/ x A. y ps <-> F/ y A. y ps ) )
10	7 9	mpbiri	|- ( A. x x = y -> F/ x A. y ps )
11	6 10	pm2.61d2	|- ( ph -> F/ x A. y ps )