Metamath Proof Explorer

Theorem axi10

Description: Axiom of Quantifier Substitution (intuitionistic logic axiom ax-10). This is just axc11n by another name. (Contributed by Jim Kingdon, 31-Dec-2017) (New usage is discouraged.)

Ref Expression
Assertion axi10 
|- ( A. x x = y -> A. y y = x )

Proof

Step Hyp Ref Expression
1 axc11n 
 |-  ( A. x x = y -> A. y y = x )