Theorem dfdif3

Description: Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022)

	Ref	Expression
Assertion	dfdif3	⊢ ( 𝐴 ∖ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 }

Proof

Step	Hyp	Ref	Expression
1		dfdif2	⊢ ( 𝐴 ∖ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵 }
2		ax6ev	⊢ ∃ 𝑦 𝑦 = 𝑥
3	2	biantrur	⊢ ( ¬ 𝑥 ∈ 𝐵 ↔ ( ∃ 𝑦 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵 ) )
4		19.41v	⊢ ( ∃ 𝑦 ( 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ( ∃ 𝑦 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵 ) )
5	3 4	bitr4i	⊢ ( ¬ 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵 ) )
6		sbalex	⊢ ( ∃ 𝑦 ( 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝐵 ) )
7		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
8	7	imbi1i	⊢ ( ( 𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 = 𝑦 → ¬ 𝑥 ∈ 𝐵 ) )
9		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
10	9	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑦 ∈ 𝐵 ) )
11	10	pm5.74i	⊢ ( ( 𝑥 = 𝑦 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 = 𝑦 → ¬ 𝑦 ∈ 𝐵 ) )
12		con2b	⊢ ( ( 𝑥 = 𝑦 → ¬ 𝑦 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 → ¬ 𝑥 = 𝑦 ) )
13		df-ne	⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
14	13	bicomi	⊢ ( ¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦 )
15	14	imbi2i	⊢ ( ( 𝑦 ∈ 𝐵 → ¬ 𝑥 = 𝑦 ) ↔ ( 𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦 ) )
16	11 12 15	3bitri	⊢ ( ( 𝑥 = 𝑦 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦 ) )
17	8 16	bitri	⊢ ( ( 𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦 ) )
18	17	albii	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦 ) )
19	5 6 18	3bitri	⊢ ( ¬ 𝑥 ∈ 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦 ) )
20		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦 ) )
21	19 20	bitr4i	⊢ ( ¬ 𝑥 ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 )
22	21	rabbii	⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵 } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 }
23	1 22	eqtri	⊢ ( 𝐴 ∖ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 }