MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-9v Unicode version

Axiom ax-9v 1632
Description: Axiom B8 of [Tarski] p. 75, which is the same as our axiom ax-9 1684 weakened with a distinct variable condition. Theorem ax9 1683 shows the derivation of ax-9 1684 from this one. (Contributed by NM, 7-Nov-2015.) (New usage is discouraged.)
Assertion
Ref Expression
ax-9v  |-  -.  A. x  -.  x  =  y
Distinct variable group:    x, y

Detailed syntax breakdown of Axiom ax-9v
StepHypRef Expression
1 vx . . . . 5  set  x
2 vy . . . . 5  set  y
31, 2weq 1620 . . . 4  wff  x  =  y
43wn 5 . . 3  wff  -.  x  =  y
54, 1wal 1532 . 2  wff  A. x  -.  x  =  y
65wn 5 1  wff  -.  A. x  -.  x  =  y
Colors of variables: wff set class
This axiom is referenced by:  ax12o10lem1  1635  ax12o10lem3  1637  ax12o10lem8  1642  ax12olem16  1650  ax10lem19  1668  ax10lem24  1673  ax10  1677  a16gALT  1679  ax9  1683  equidK  28235  a4imK  28249  a4imvK  28250  ax12o10lem1X  28282  ax12o10lem3X  28284  ax12o10lem3K  28285  ax12o10lem8K  28294  ax12o10lem8X  28295  ax12olem16K  28311  ax12olem16X  28312  ax10lem19X  28338  ax10lem24X  28343  ax10X  28347  a16gALTX  28348  ax9X  28352  a12stdy1-x12  28361  ax10lem17ALT  28373  a12study10  28386  a12study10n  28387  ax9OLD  28409
  Copyright terms: Public domain W3C validator