Axiom ax-nur 214

Description: Variables can be renamed without changing the meaning of an expression.

Assertion

Ref	Expression
ax-nur	⊦ (νx[u ≪ x] 𝜑 ⊸ νy[u ≪ y] 𝜑)

Detailed syntax breakdown of Axiom ax-nur

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vu	. . . . 5 var u
3	2	nvar 203	. . . 4 nilad u
4		vx	. . . . 5 var x
5	4	nvar 203	. . . 4 nilad x
6	1, 3, 5	wse 204	. . 3 wff [u ≪ x] 𝜑
7	6, 4	wnu 206	. 2 wff νx[u ≪ x] 𝜑
8		vy	. . . . 5 var y
9	8	nvar 203	. . . 4 nilad y
10	1, 3, 9	wse 204	. . 3 wff [u ≪ y] 𝜑
11	10, 8	wnu 206	. 2 wff νy[u ≪ y] 𝜑
12	7, 11	wli 61	1 wff (νx[u ≪ x] 𝜑 ⊸ νy[u ≪ y] 𝜑)

This axiom is referenced by: (None)