Theorem dfdif3

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

	Ref	Expression
Assertion	dfdif3	|- ( A \ B ) = { x e. A | A. y e. B x =/= y }

Proof

Step	Hyp	Ref	Expression
1		dfdif2	|- ( A \ B ) = { x e. A | -. x e. B }
2		ax6ev	|- E. y y = x
3	2	biantrur	|- ( -. x e. B <-> ( E. y y = x /\ -. x e. B ) )
4		19.41v	|- ( E. y ( y = x /\ -. x e. B ) <-> ( E. y y = x /\ -. x e. B ) )
5	3 4	bitr4i	|- ( -. x e. B <-> E. y ( y = x /\ -. x e. B ) )
6		sbalex	|- ( E. y ( y = x /\ -. x e. B ) <-> A. y ( y = x -> -. x e. B ) )
7		equcom	|- ( y = x <-> x = y )
8	7	imbi1i	|- ( ( y = x -> -. x e. B ) <-> ( x = y -> -. x e. B ) )
9		eleq1w	|- ( x = y -> ( x e. B <-> y e. B ) )
10	9	notbid	|- ( x = y -> ( -. x e. B <-> -. y e. B ) )
11	10	pm5.74i	|- ( ( x = y -> -. x e. B ) <-> ( x = y -> -. y e. B ) )
12		con2b	|- ( ( x = y -> -. y e. B ) <-> ( y e. B -> -. x = y ) )
13		df-ne	|- ( x =/= y <-> -. x = y )
14	13	bicomi	|- ( -. x = y <-> x =/= y )
15	14	imbi2i	|- ( ( y e. B -> -. x = y ) <-> ( y e. B -> x =/= y ) )
16	11 12 15	3bitri	|- ( ( x = y -> -. x e. B ) <-> ( y e. B -> x =/= y ) )
17	8 16	bitri	|- ( ( y = x -> -. x e. B ) <-> ( y e. B -> x =/= y ) )
18	17	albii	|- ( A. y ( y = x -> -. x e. B ) <-> A. y ( y e. B -> x =/= y ) )
19	5 6 18	3bitri	|- ( -. x e. B <-> A. y ( y e. B -> x =/= y ) )
20		df-ral	|- ( A. y e. B x =/= y <-> A. y ( y e. B -> x =/= y ) )
21	19 20	bitr4i	|- ( -. x e. B <-> A. y e. B x =/= y )
22	21	rabbii	|- { x e. A | -. x e. B } = { x e. A | A. y e. B x =/= y }
23	1 22	eqtri	|- ( A \ B ) = { x e. A | A. y e. B x =/= y }