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

Axiom ax-10d 2238
Description: Distinct varable version of ax10 1884. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
ax-10d  |-  ( A. x  x  =  y  ->  A. y  y  =  x )
Distinct variable group:    x, y

Detailed syntax breakdown of Axiom ax-10d
StepHypRef Expression
1 vx . . . 4  set  x
2 vy . . . 4  set  y
31, 2weq 1624 . . 3  wff  x  =  y
43, 1wal 1527 . 2  wff  A. x  x  =  y
52, 1weq 1624 . . 3  wff  y  =  x
65, 2wal 1527 . 2  wff  A. y 
y  =  x
74, 6wi 4 1  wff  ( A. x  x  =  y  ->  A. y  y  =  x )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator