Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Version of dral1 with a disjoint variable condition, which does not require ax-13 . Remark: the corresponding versions for dral2 and drex2 are instances of albidv and exbidv respectively. (Contributed by NM, 24-Nov-1994) (Revised by BJ, 17-Jun-2019) Base the proof on ax12v . (Revised by Wolf Lammen, 30-Mar-2024) Avoid ax-10 . (Revised by Gino Giotto, 18-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | dral1v.1 | |- ( A. x x = y -> ( ph <-> ps ) ) |
|
| Assertion | dral1v | |- ( A. x x = y -> ( A. x ph <-> A. y ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dral1v.1 | |- ( A. x x = y -> ( ph <-> ps ) ) |
|
| 2 | hbaev | |- ( A. x x = y -> A. x A. x x = y ) |
|
| 3 | 2 1 | albidh | |- ( A. x x = y -> ( A. x ph <-> A. x ps ) ) |
| 4 | axc11v | |- ( A. x x = y -> ( A. x ps -> A. y ps ) ) |
|
| 5 | axc11rv | |- ( A. x x = y -> ( A. y ps -> A. x ps ) ) |
|
| 6 | 4 5 | impbid | |- ( A. x x = y -> ( A. x ps <-> A. y ps ) ) |
| 7 | 3 6 | bitrd | |- ( A. x x = y -> ( A. x ph <-> A. y ps ) ) |