Theorem dral1v

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)

	Ref	Expression
Hypothesis	dral1v.1	|- ( A. x x = y -> ( ph <-> ps ) )
Assertion	dral1v	|- ( A. x x = y -> ( A. x ph <-> A. y ps ) )

Proof

Step	Hyp	Ref	Expression
1		dral1v.1	|- ( A. x x = y -> ( ph <-> ps ) )
2		nfa1	|- F/ x A. x x = y
3	2 1	albid	|- ( 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 ) )