Metamath Proof Explorer


Theorem bj-axc10v

Description: Version of axc10 with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 14-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-axc10v x x = y x φ φ

Proof

Step Hyp Ref Expression
1 ax6v ¬ x ¬ x = y
2 con3 x = y x φ ¬ x φ ¬ x = y
3 2 al2imi x x = y x φ x ¬ x φ x ¬ x = y
4 1 3 mtoi x x = y x φ ¬ x ¬ x φ
5 axc7 ¬ x ¬ x φ φ
6 4 5 syl x x = y x φ φ