MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax7v Structured version   Visualization version   GIF version

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

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

Assertion
Ref Expression
ax7v (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
Distinct variable group:   𝑥,𝑦

Proof of Theorem ax7v
StepHypRef Expression
1 ax-7 2006 1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-7 2006
This theorem is referenced by:  ax7v1  2008  ax7v2  2009
  Copyright terms: Public domain W3C validator