Syntax Definition wel 322

Description: Set element predicate. For the purposes of predicate logic, it's just an arbitrary operator.

Hypotheses

Ref	Expression
vx	var x
vy	var y

Assertion

Ref	Expression
wel	wff x ∈ y

This syntax is primitive. The first axiom using it is ax-eleq1 328.