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

Axiom ax-8 2147
Description: Axiom of Left Equality for Binary Predicate. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the left-hand side of an arbitrary binary predicate , which we will use for the set membership relation when set theory is introduced. This axiom scheme is a sub-scheme of Axiom Scheme B8 of system S2 of [Tarski], p. 75, whose general form cannot be represented with our notation. Also appears as Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). "Non-logical" means that the predicate is not a primitive of predicate calculus proper but instead is an extension to it. "Binary" means that the predicate has two arguments. In a system of predicate calculus with equality, like ours, equality is not usually considered to be a non-logical predicate. In systems of predicate calculus without equality, it typically would be.

We prove in ax8 2151 that this axiom can be recovered from its weakened version ax8v 2148 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-8 2147 should be ax8v 2148. See the comment of ax8v 2148 for more details on these matters. (Contributed by NM, 30-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax8 2151 instead. (New usage is discouraged.)

Assertion
Ref Expression
ax-8 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))

Detailed syntax breakdown of Axiom ax-8
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 vy . . 3 setvar 𝑦
31, 2weq 2043 . 2 wff 𝑥 = 𝑦
4 vz . . . 4 setvar 𝑧
51, 4wel 2146 . . 3 wff 𝑥𝑧
62, 4wel 2146 . . 3 wff 𝑦𝑧
75, 6wi 4 . 2 wff (𝑥𝑧𝑦𝑧)
83, 7wi 4 1 wff (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
Colors of variables: wff setvar class
This axiom is referenced by:  ax8v  2148
  Copyright terms: Public domain W3C validator