Theorem raldifsnb

Description: Restricted universal quantification on a class difference with a singleton in terms of an implication. (Contributed by Alexander van der Vekens, 26-Jan-2018)

	Ref	Expression
Assertion	raldifsnb	|- ( A. x e. A ( x =/= Y -> ph ) <-> A. x e. ( A \ { Y } ) ph )

Proof

Step	Hyp	Ref	Expression
1		velsn	|- ( x e. { Y } <-> x = Y )
2		nnel	|- ( -. x e/ { Y } <-> x e. { Y } )
3		nne	|- ( -. x =/= Y <-> x = Y )
4	1 2 3	3bitr4ri	|- ( -. x =/= Y <-> -. x e/ { Y } )
5	4	con4bii	|- ( x =/= Y <-> x e/ { Y } )
6	5	imbi1i	|- ( ( x =/= Y -> ph ) <-> ( x e/ { Y } -> ph ) )
7	6	ralbii	|- ( A. x e. A ( x =/= Y -> ph ) <-> A. x e. A ( x e/ { Y } -> ph ) )
8		raldifb	|- ( A. x e. A ( x e/ { Y } -> ph ) <-> A. x e. ( A \ { Y } ) ph )
9	7 8	bitri	|- ( A. x e. A ( x =/= Y -> ph ) <-> A. x e. ( A \ { Y } ) ph )