Syntax Definition wel 803

Description: Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "x is an element of y," "x is a member of y," "x belongs to y," or "y contains x." Note: The phrase "y includes x" means "x is a subset of y"; to use it also for x ∈ y (as some authors occasionally do) is poor form and causes confusion.

Hypotheses

Ref	Expression
vx	set x
vy	set y

Assertion

Ref	Expression
wel	wff x ∈ y

This syntax is primitive. The first axiom using it is ax-13 804.

metamath.org