Theorem rabdif

Description: Move difference in and out of a restricted class abstraction. (Contributed by Steven Nguyen, 6-Jun-2023)

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

Proof

Step	Hyp	Ref	Expression
1		indif2	|- ( { x | ph } i^i ( A \ B ) ) = ( ( { x | ph } i^i A ) \ B )
2		dfrab2	|- { x e. ( A \ B ) | ph } = ( { x | ph } i^i ( A \ B ) )
3		dfrab2	|- { x e. A | ph } = ( { x | ph } i^i A )
4	3	difeq1i	|- ( { x e. A | ph } \ B ) = ( ( { x | ph } i^i A ) \ B )
5	1 2 4	3eqtr4ri	|- ( { x e. A | ph } \ B ) = { x e. ( A \ B ) | ph }