Theorem ax7v 2044

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

In ax7v 2044, it is still allowed to substitute the same variable for 𝑥 and 𝑧, or the same variable for 𝑦 and 𝑧. Therefore, ax7v 2044 "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 2049 and equid 2047 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 2051 instead. (New usage is discouraged.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Proof of Theorem ax7v

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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-7 2043

This theorem is used by:  ax7v1  2045  ax7v2  2046