Metamath Proof Explorer


Theorem axc10

Description: Show that the original axiom ax-c10 can be derived from ax6 and axc7 (on top of propositional calculus, ax-gen , and ax-4 ). See ax6fromc10 for the rederivation of ax6 from ax-c10 .

Normally, axc10 should be used rather than ax-c10 , except by theorems specifically studying the latter's properties. Usage of this theorem has been discouraged later on to avoid ax-13 propagation. Check out bj-axc10v for a weaker version requiring fewer axioms. (Contributed by NM, 5-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax6
 |-  -. A. x -. x = y
2 con3
 |-  ( ( x = y -> A. x ph ) -> ( -. A. x ph -> -. x = y ) )
3 2 al2imi
 |-  ( A. x ( x = y -> A. x ph ) -> ( A. x -. A. x ph -> A. x -. x = y ) )
4 1 3 mtoi
 |-  ( A. x ( x = y -> A. x ph ) -> -. A. x -. A. x ph )
5 axc7
 |-  ( -. A. x -. A. x ph -> ph )
6 4 5 syl
 |-  ( A. x ( x = y -> A. x ph ) -> ph )