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 biorfi ( ( 𝜑 ∧ ¬ 𝑥𝐵 ) ↔ ( ( 𝜑 ∧ ¬ 𝑥𝐵 ) ∨ ( 𝜑 ∧ ¬ 𝜑 ) ) )
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 ( { 𝑥𝐴𝜑 } ∖ { 𝑥𝐵𝜑 } ) = { 𝑥 ∈ ( 𝐴𝐵 ) ∣ 𝜑 }