Theorem disjOLD

Description: Obsolete version of disj as of 28-Jun-2024. (Contributed by NM, 17-Feb-2004) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	disjOLD	|- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )

Proof

Step	Hyp	Ref	Expression
1		df-in	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
2	1	eqeq1i	|- ( ( A i^i B ) = (/) <-> { x | ( x e. A /\ x e. B ) } = (/) )
3		abeq1	|- ( { x | ( x e. A /\ x e. B ) } = (/) <-> A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
4		imnan	|- ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
5		noel	|- -. x e. (/)
6	5	nbn	|- ( -. ( x e. A /\ x e. B ) <-> ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
7	4 6	bitr2i	|- ( ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> ( x e. A -> -. x e. B ) )
8	7	albii	|- ( A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> A. x ( x e. A -> -. x e. B ) )
9	2 3 8	3bitri	|- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
10		df-ral	|- ( A. x e. A -. x e. B <-> A. x ( x e. A -> -. x e. B ) )
11	9 10	bitr4i	|- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )