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

Metamath Proof Explorer

Theorem difrab2

Description: Difference of two restricted class abstractions. Compare with difrab . (Contributed by Thierry Arnoux, 3-Jan-2022)

Ref Expression
Assertion difrab2 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) = { 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∣ 𝜑 }

Proof

Step Hyp Ref Expression
1 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝜑 }
2 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐵 ∣ 𝜑 }
3 1 2 nfdif ⊢ Ⅎ 𝑥 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐵 ∣ 𝜑 } )
4 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∣ 𝜑 }
5 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
6 5 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) )
7 andi ⊢ ( ( 𝜑 ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) ) ↔ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐵 ) ∨ ( 𝜑 ∧ ¬ 𝜑 ) ) )
8 pm3.24 ⊢ ¬ ( 𝜑 ∧ ¬ 𝜑 )
9 8 biorfri ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐵 ) ∨ ( 𝜑 ∧ ¬ 𝜑 ) ) )
10 ancom ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ( ¬ 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
11 7 9 10 3bitr2i ⊢ ( ( 𝜑 ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) ) ↔ ( ¬ 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
12 11 anbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ¬ 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
13 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) ) ) )
14 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ¬ 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
15 12 13 14 3bitr4i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) )
16 6 15 bitr4i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) ) )
17 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∣ 𝜑 } ↔ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝜑 ) )
18 eldif ⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) ↔ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∧ ¬ 𝑥 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) )
19 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
20 ianor ⊢ ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) )
21 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
22 20 21 xchnxbir ⊢ ( ¬ 𝑥 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) )
23 19 22 anbi12i ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∧ ¬ 𝑥 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) ) )
24 18 23 bitri ⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝜑 ) ) )
25 16 17 24 3bitr4ri ⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) ↔ 𝑥 ∈ { 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∣ 𝜑 } )
26 3 4 25 eqri ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) = { 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∣ 𝜑 }