Theorem raldifsni

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

	Ref	Expression
Assertion	raldifsni	|- ( A. x e. ( A \ { B } ) -. ph <-> A. x e. A ( ph -> x = B ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	|- ( x e. ( A \ { B } ) <-> ( x e. A /\ x =/= B ) )
2	1	imbi1i	|- ( ( x e. ( A \ { B } ) -> -. ph ) <-> ( ( x e. A /\ x =/= B ) -> -. ph ) )
3		impexp	|- ( ( ( x e. A /\ x =/= B ) -> -. ph ) <-> ( x e. A -> ( x =/= B -> -. ph ) ) )
4		df-ne	|- ( x =/= B <-> -. x = B )
5	4	imbi1i	|- ( ( x =/= B -> -. ph ) <-> ( -. x = B -> -. ph ) )
6		con34b	|- ( ( ph -> x = B ) <-> ( -. x = B -> -. ph ) )
7	5 6	bitr4i	|- ( ( x =/= B -> -. ph ) <-> ( ph -> x = B ) )
8	7	imbi2i	|- ( ( x e. A -> ( x =/= B -> -. ph ) ) <-> ( x e. A -> ( ph -> x = B ) ) )
9	2 3 8	3bitri	|- ( ( x e. ( A \ { B } ) -> -. ph ) <-> ( x e. A -> ( ph -> x = B ) ) )
10	9	ralbii2	|- ( A. x e. ( A \ { B } ) -. ph <-> A. x e. A ( ph -> x = B ) )