Theorem ax7v 1982

Description: Weakened version of ax-7 1981, with a dv condition on 𝑥, 𝑦. This should be the only proof referencing ax-7 1981, and it should be referenced only by its two weakened versions ax7v1 1983 and ax7v2 1984, from which ax-7 1981 is then rederived as ax7 1989, which shows that either ax7v 1982 or the conjunction of ax7v1 1983 and ax7v2 1984 is sufficient.

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

Assertion

Ref	Expression
ax7v	⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))

Distinct variable group:   𝑥,𝑦

Proof of Theorem ax7v

Step	Hyp	Ref	Expression
1		ax-7 1981	1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-7 1981

This theorem is referenced by:  ax7v1  1983  ax7v2  1984