Metamath Proof Explorer

Axiom ax-10d

Description: Distinct variable version of axc11n . (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion ax-10d 
|- ( A. x x = y -> A. y y = x )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 
 |-  x
1 0 cv 
 |-  x
2 vy 
 |-  y
3 2 cv 
 |-  y
4 1 3 wceq 
 |-  x = y
5 4 0 wal 
 |-  A. x x = y
6 3 1 wceq 
 |-  y = x
7 6 2 wal 
 |-  A. y y = x
8 5 7 wi 
 |-  ( A. x x = y -> A. y y = x )