This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }