Theorem dfdif3

Description: Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022) (Proof shortened by SN, 15-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		dfdif2	⊢ ( 𝐴 ∖ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵 }
2		nelb	⊢ ( ¬ 𝑥 ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 𝑦 ≠ 𝑥 )
3		necom	⊢ ( 𝑦 ≠ 𝑥 ↔ 𝑥 ≠ 𝑦 )
4	3	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐵 𝑦 ≠ 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 )
5	2 4	bitri	⊢ ( ¬ 𝑥 ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 )
6	1 5	rabbieq	⊢ ( 𝐴 ∖ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 }