Theorem notrab

Description: Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	notrab	⊢ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		difab	⊢ ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∖ { 𝑥 ∣ 𝜑 } ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) }
2		difin	⊢ ( 𝐴 ∖ ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } ) ) = ( 𝐴 ∖ { 𝑥 ∣ 𝜑 } )
3		dfrab3	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } )
4	3	difeq2i	⊢ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) = ( 𝐴 ∖ ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } ) )
5		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 } = 𝐴
6	5	difeq1i	⊢ ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∖ { 𝑥 ∣ 𝜑 } ) = ( 𝐴 ∖ { 𝑥 ∣ 𝜑 } )
7	2 4 6	3eqtr4i	⊢ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) = ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∖ { 𝑥 ∣ 𝜑 } )
8		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) }
9	1 7 8	3eqtr4i	⊢ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }