Description: Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016) (Proof shortened by Wolf Lammen, 5-May-2018) Usage of this theorem is discouraged because it depends on ax-13 . Use nfbidv instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | dral1.1 | |- ( A. x x = y -> ( ph <-> ps ) ) |
|
| Assertion | drnf2 | |- ( A. x x = y -> ( F/ z ph <-> F/ z ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dral1.1 | |- ( A. x x = y -> ( ph <-> ps ) ) |
|
| 2 | nfae | |- F/ z A. x x = y |
|
| 3 | 2 1 | nfbidf | |- ( A. x x = y -> ( F/ z ph <-> F/ z ps ) ) |