Theorem raldifb

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

	Ref	Expression
Assertion	raldifb	|- ( A. x e. A ( x e/ B -> ph ) <-> A. x e. ( A \ B ) ph )

Proof

Step	Hyp	Ref	Expression
1		impexp	|- ( ( ( x e. A /\ x e/ B ) -> ph ) <-> ( x e. A -> ( x e/ B -> ph ) ) )
2		df-nel	|- ( x e/ B <-> -. x e. B )
3	2	anbi2i	|- ( ( x e. A /\ x e/ B ) <-> ( x e. A /\ -. x e. B ) )
4		eldif	|- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
5	3 4	bitr4i	|- ( ( x e. A /\ x e/ B ) <-> x e. ( A \ B ) )
6	5	imbi1i	|- ( ( ( x e. A /\ x e/ B ) -> ph ) <-> ( x e. ( A \ B ) -> ph ) )
7	1 6	bitr3i	|- ( ( x e. A -> ( x e/ B -> ph ) ) <-> ( x e. ( A \ B ) -> ph ) )
8	7	ralbii2	|- ( A. x e. A ( x e/ B -> ph ) <-> A. x e. ( A \ B ) ph )