This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )