Syntax Definition wdisj 4010

Description: Extend wff notation to include the statement that a family of classes B ( x ), for x e. A, is a disjoint family.

Hypotheses

Ref	Expression
vx	setvar x
cA	class A
cB	class B

Assertion

Ref	Expression
wdisj	wff Disj x e. A B

See definition df-disj 4011 for more information.