Theorem ax7v

Description: Weakened version of ax-7 , with a disjoint variable condition on x , y . This should be the only proof referencing ax-7 , and it should be referenced only by its two weakened versions ax7v1 and ax7v2 , from which ax-7 is then rederived as ax7 , which shows that either ax7v or the conjunction of ax7v1 and ax7v2 is sufficient.

In ax7v , it is still allowed to substitute the same variable for x and z , or the same variable for y and z . Therefore, ax7v "bundles" (a term coined by Raph Levien) its "principal instance" ( x = y -> ( x = z -> y = z ) ) with x , y , z distinct, and its "degenerate instances" ( x = y -> ( x = x -> y = x ) ) and ( x = y -> ( x = y -> y = y ) ) with x , y distinct. These degenerate instances are for instance used in the proofs of equcomiv and equid respectively. (Contributed by BJ, 7-Dec-2020) Use ax7 instead. (New usage is discouraged.)

	Ref	Expression
Assertion	ax7v	|- ( x = y -> ( x = z -> y = z ) )

Proof

Step	Hyp	Ref	Expression
1		ax-7	|- ( x = y -> ( x = z -> y = z ) )