wich - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > wich		Structured version Visualization version GIF version

Syntax Definition wich 44897

Description: Extend wff notation to include the propery of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. Read this notation as "𝑥 and 𝑦 are interchangeable in wff 𝜑".

**Hypotheses**
Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥
vy	setvar 𝑦

**Assertion**
Ref	Expression
wich	wff [𝑥⇄𝑦]𝜑

See definition df-ich 44898 for more information.

Colors of variables: wff setvar class

W3C validator