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 ⊢Ⅎ_xx∈A|φ
2 nfrab1 ⊢Ⅎ_xx∈B|φ
3 1 2 nfdif ⊢Ⅎ_xx∈A|φ∖x∈B|φ
4 nfrab1 ⊢Ⅎ_xx∈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|φ