Metamath Proof Explorer

Axiom ax-11d

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

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

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 wph 
 |-  ph
6 5 2 wal 
 |-  A. y ph
7 4 5 wi 
 |-  ( x = y -> ph )
8 7 0 wal 
 |-  A. x ( x = y -> ph )
9 6 8 wi 
 |-  ( A. y ph -> A. x ( x = y -> ph ) )
10 4 9 wi 
 |-  ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )