Syntax Definition wff-elemof 7

Description: If '𝑡' and '𝑢' are terms, then '𝑡 ∈ 𝑢' is a well formed formula.

Hypotheses

Ref	Expression
term-t	term 𝑡
term-u	term 𝑢

Assertion

Ref	Expression
wff-elemof	wff 𝑡 ∈ 𝑢

This syntax is primitive. The first axiom using it is ax-L8-inl 20.