Syntax Definition wdisj 3901

Description: Extend wff notation to include the statement that a family of classes 𝐵(𝑥), for 𝑥 ∈ 𝐴, is a disjoint family.

Hypotheses

Ref	Expression
vx	setvar 𝑥
cA	class 𝐴
cB	class 𝐵

Assertion

Ref	Expression
wdisj	wff Disj 𝑥 ∈ 𝐴 𝐵

See definition df-disj 3902 for more information.