Syntax Definition wdisj 3901

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 3902 for more information.