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	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ) = { 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∣ 𝜑 }