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  a12stdy1-x12  27800  ax10lem17ALT  27812  a12study10  27825  a12study10n  27826  ax9OLD  27848
  Copyright terms: Public domain W3C validator