Theorem dfdisj2

Description: Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017)

	Ref	Expression
Assertion	dfdisj2	|- ( Disj_ x e. A B <-> A. y E* x ( x e. A /\ y e. B ) )

Proof

Step	Hyp	Ref	Expression
1		df-disj	|- ( Disj_ x e. A B <-> A. y E* x e. A y e. B )
2		df-rmo	|- ( E* x e. A y e. B <-> E* x ( x e. A /\ y e. B ) )
3	2	albii	|- ( A. y E* x e. A y e. B <-> A. y E* x ( x e. A /\ y e. B ) )
4	1 3	bitri	|- ( Disj_ x e. A B <-> A. y E* x ( x e. A /\ y e. B ) )