Description: Variation on nfald 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 nfald 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 | nfald2 | |- ( ph -> F/ x A. y ps ) |
| 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 ) |