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  28115  a4imK  28129  a4imvK  28130  ax12o10lem1X  28162  ax12o10lem3X  28164  ax12o10lem3K  28165  ax12o10lem8K  28174  ax12o10lem8X  28175  ax12olem16K  28191  ax12olem16X  28192  ax10lem19X  28218  ax10lem24X  28223  ax10X  28227  a16gALTX  28228  ax9X  28232  a12stdy1-x12  28241  ax10lem17ALT  28253  a12study10  28266  a12study10n  28267  ax9OLD  28289
  Copyright terms: Public domain W3C validator