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 ⊢ x ∈ A | φ ∖ x ∈ B | φ = x ∈ A ∖ B | φ

Proof

Step Hyp Ref Expression
1 nfrab1 ⊢ Ⅎ _ x x ∈ A | φ
2 nfrab1 ⊢ Ⅎ _ x x ∈ B | φ
3 1 2 nfdif ⊢ Ⅎ _ x x ∈ A | φ ∖ x ∈ B | φ
4 nfrab1 ⊢ Ⅎ _ x x ∈ A ∖ B | φ
5 eldif ⊢ x ∈ A ∖ B ↔ x ∈ A ∧ ¬ x ∈ B
6 5 anbi1i ⊢ x ∈ A ∖ B ∧ φ ↔ x ∈ A ∧ ¬ x ∈ B ∧ φ
7 andi ⊢ φ ∧ ¬ x ∈ B ∨ ¬ φ ↔ φ ∧ ¬ x ∈ B ∨ φ ∧ ¬ φ
8 pm3.24 ⊢ ¬ φ ∧ ¬ φ
9 8 biorfi ⊢ φ ∧ ¬ x ∈ B ↔ φ ∧ ¬ x ∈ B ∨ φ ∧ ¬ φ
10 ancom ⊢ φ ∧ ¬ x ∈ B ↔ ¬ x ∈ B ∧ φ
11 7 9 10 3bitr2i ⊢ φ ∧ ¬ x ∈ B ∨ ¬ φ ↔ ¬ x ∈ B ∧ φ
12 11 anbi2i ⊢ x ∈ A ∧ φ ∧ ¬ x ∈ B ∨ ¬ φ ↔ x ∈ A ∧ ¬ x ∈ B ∧ φ
13 anass ⊢ x ∈ A ∧ φ ∧ ¬ x ∈ B ∨ ¬ φ ↔ x ∈ A ∧ φ ∧ ¬ x ∈ B ∨ ¬ φ
14 anass ⊢ x ∈ A ∧ ¬ x ∈ B ∧ φ ↔ x ∈ A ∧ ¬ x ∈ B ∧ φ
15 12 13 14 3bitr4i ⊢ x ∈ A ∧ φ ∧ ¬ x ∈ B ∨ ¬ φ ↔ x ∈ A ∧ ¬ x ∈ B ∧ φ
16 6 15 bitr4i ⊢ x ∈ A ∖ B ∧ φ ↔ x ∈ A ∧ φ ∧ ¬ x ∈ B ∨ ¬ φ
17 rabid ⊢ x ∈ x ∈ A ∖ B | φ ↔ x ∈ A ∖ B ∧ φ
18 eldif ⊢ x ∈ x ∈ A | φ ∖ x ∈ B | φ ↔ x ∈ x ∈ A | φ ∧ ¬ x ∈ x ∈ B | φ
19 rabid ⊢ x ∈ x ∈ A | φ ↔ x ∈ A ∧ φ
20 ianor ⊢ ¬ x ∈ B ∧ φ ↔ ¬ x ∈ B ∨ ¬ φ
21 rabid ⊢ x ∈ x ∈ B | φ ↔ x ∈ B ∧ φ
22 20 21 xchnxbir ⊢ ¬ x ∈ x ∈ B | φ ↔ ¬ x ∈ B ∨ ¬ φ
23 19 22 anbi12i ⊢ x ∈ x ∈ A | φ ∧ ¬ x ∈ x ∈ B | φ ↔ x ∈ A ∧ φ ∧ ¬ x ∈ B ∨ ¬ φ
24 18 23 bitri ⊢ x ∈ x ∈ A | φ ∖ x ∈ B | φ ↔ x ∈ A ∧ φ ∧ ¬ x ∈ B ∨ ¬ φ
25 16 17 24 3bitr4ri ⊢ x ∈ x ∈ A | φ ∖ x ∈ B | φ ↔ x ∈ x ∈ A ∖ B | φ
26 3 4 25 eqri ⊢ x ∈ A | φ ∖ x ∈ B | φ = x ∈ A ∖ B | φ