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

Metamath Proof Explorer

Theorem difrab

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

Ref Expression
Assertion difrab ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ ¬ 𝜓 ) }

Proof

Step Hyp Ref Expression
1 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) }
3 1 2 difeq12i ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∖ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } )
4 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ ¬ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ ¬ 𝜓 ) ) }
5 difab ⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∖ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) }
6 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ ¬ 𝜓 ) ) )
7 simpr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝜓 )
8 7 con3i ⊢ ( ¬ 𝜓 → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
9 8 anim2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ 𝜓 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
10 pm3.2 ⊢ ( 𝑥 ∈ 𝐴 → ( 𝜓 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
11 10 adantr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝜓 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
12 11 con3d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ¬ 𝜓 ) )
13 12 imdistani ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ 𝜓 ) )
14 9 13 impbii ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ 𝜓 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
15 6 14 bitr3i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ ¬ 𝜓 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
16 15 abbii ⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ ¬ 𝜓 ) ) } = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) }
17 5 16 eqtr4i ⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∖ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ ¬ 𝜓 ) ) }
18 4 17 eqtr4i ⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ ¬ 𝜓 ) } = ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∖ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } )
19 3 18 eqtr4i ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ ¬ 𝜓 ) }