Metamath Proof Explorer

Axiom ax-9d1

Description: Distinct variable version of ax-6 , equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion ax-9d1 
|- -. A. x -. x = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 
 |-  x
1 0 cv 
 |-  x
2 1 1 wceq 
 |-  x = x
3 2 wn 
 |-  -. x = x
4 3 0 wal 
 |-  A. x -. x = x
5 4 wn 
 |-  -. A. x -. x = x