Metamath Proof Explorer

Theorem axc16nfALT

Description: Alternate proof of axc16nf , shorter but requiring ax-11 and ax-13 . (Contributed by Mario Carneiro, 7-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axc16nfALT 
|- ( A. x x = y -> F/ z ph )

Proof

Step Hyp Ref Expression
1 nfae 
 |-  F/ z A. x x = y
2 axc16g 
 |-  ( A. x x = y -> ( ph -> A. z ph ) )
3 1 2 nf5d 
 |-  ( A. x x = y -> F/ z ph )