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