Syntax Definition wre 205

Description: Recieving operator. Reads from X and scopes the result to y.

Hypotheses

Ref	Expression
wph	wff 𝜑
vy	var y
nx	nilad X

Assertion

Ref	Expression
wre	wff [X ≫ y] 𝜑

This syntax is primitive. The first axiom using it is ax-ref 211.