Metamath Proof Explorer


Theorem bj-rest10b

Description: Alternate version of bj-rest10 . (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-rest10b X V X 𝑡 =

Proof

Step Hyp Ref Expression
1 eldif X V X V ¬ X
2 0ex V
3 2 elsn2 X X =
4 neqne ¬ X = X
5 3 4 sylnbi ¬ X X
6 5 anim2i X V ¬ X X V X
7 1 6 sylbi X V X V X
8 bj-rest10 X V X X 𝑡 =
9 8 imp X V X X 𝑡 =
10 7 9 syl X V X 𝑡 =