# Metamath Proof Explorer

## Theorem difrab

Description: Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004)

Ref Expression
Assertion difrab ${⊢}\left\{{x}\in {A}|{\phi }\right\}\setminus \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|\left({\phi }\wedge ¬{\psi }\right)\right\}$

### Proof

Step Hyp Ref Expression
1 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
2 df-rab ${⊢}\left\{{x}\in {A}|{\psi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}$
3 1 2 difeq12i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\setminus \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\setminus \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}$
4 df-rab ${⊢}\left\{{x}\in {A}|\left({\phi }\wedge ¬{\psi }\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge \left({\phi }\wedge ¬{\psi }\right)\right)\right\}$
5 difab ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\setminus \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}=\left\{{x}|\left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬\left({x}\in {A}\wedge {\psi }\right)\right)\right\}$
6 anass ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬{\psi }\right)↔\left({x}\in {A}\wedge \left({\phi }\wedge ¬{\psi }\right)\right)$
7 simpr ${⊢}\left({x}\in {A}\wedge {\psi }\right)\to {\psi }$
8 7 con3i ${⊢}¬{\psi }\to ¬\left({x}\in {A}\wedge {\psi }\right)$
9 8 anim2i ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬{\psi }\right)\to \left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬\left({x}\in {A}\wedge {\psi }\right)\right)$
10 pm3.2 ${⊢}{x}\in {A}\to \left({\psi }\to \left({x}\in {A}\wedge {\psi }\right)\right)$
11 10 adantr ${⊢}\left({x}\in {A}\wedge {\phi }\right)\to \left({\psi }\to \left({x}\in {A}\wedge {\psi }\right)\right)$
12 11 con3d ${⊢}\left({x}\in {A}\wedge {\phi }\right)\to \left(¬\left({x}\in {A}\wedge {\psi }\right)\to ¬{\psi }\right)$
13 12 imdistani ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬\left({x}\in {A}\wedge {\psi }\right)\right)\to \left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬{\psi }\right)$
14 9 13 impbii ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬{\psi }\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬\left({x}\in {A}\wedge {\psi }\right)\right)$
15 6 14 bitr3i ${⊢}\left({x}\in {A}\wedge \left({\phi }\wedge ¬{\psi }\right)\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬\left({x}\in {A}\wedge {\psi }\right)\right)$
16 15 abbii ${⊢}\left\{{x}|\left({x}\in {A}\wedge \left({\phi }\wedge ¬{\psi }\right)\right)\right\}=\left\{{x}|\left(\left({x}\in {A}\wedge {\phi }\right)\wedge ¬\left({x}\in {A}\wedge {\psi }\right)\right)\right\}$
17 5 16 eqtr4i ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\setminus \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge \left({\phi }\wedge ¬{\psi }\right)\right)\right\}$
18 4 17 eqtr4i ${⊢}\left\{{x}\in {A}|\left({\phi }\wedge ¬{\psi }\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\setminus \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}$
19 3 18 eqtr4i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\setminus \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|\left({\phi }\wedge ¬{\psi }\right)\right\}$