Metamath Proof Explorer


Theorem raldifsni

Description: Rearrangement of a property of a singleton difference. (Contributed by Stefan O'Rear, 27-Feb-2015)

Ref Expression
Assertion raldifsni xAB¬φxAφx=B

Proof

Step Hyp Ref Expression
1 eldifsn xABxAxB
2 1 imbi1i xAB¬φxAxB¬φ
3 impexp xAxB¬φxAxB¬φ
4 df-ne xB¬x=B
5 4 imbi1i xB¬φ¬x=B¬φ
6 con34b φx=B¬x=B¬φ
7 5 6 bitr4i xB¬φφx=B
8 7 imbi2i xAxB¬φxAφx=B
9 2 3 8 3bitri xAB¬φxAφx=B
10 9 ralbii2 xAB¬φxAφx=B