Theorem wl-sb9v

Description: Commutation of quantification and substitution variables based on fewer axioms than sb9 . (Contributed by Wolf Lammen, 27-Apr-2025)

	Ref	Expression
Assertion	wl-sb9v	$$⊢\forall x\left[x/y\right]\phi \leftrightarrow \forall y\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		alcom	$$⊢\forall x\forall y\left(x=y\to \phi \right)\leftrightarrow \forall y\forall x\left(x=y\to \phi \right)$$
2		sb6	$$⊢\left[x/y\right]\phi \leftrightarrow \forall y\left(y=x\to \phi \right)$$
3		equcom	$$⊢y=x\leftrightarrow x=y$$
4	3	imbi1i	$$⊢\left(y=x\to \phi \right)\leftrightarrow \left(x=y\to \phi \right)$$
5	4	albii	$$⊢\forall y\left(y=x\to \phi \right)\leftrightarrow \forall y\left(x=y\to \phi \right)$$
6	2 5	bitri	$$⊢\left[x/y\right]\phi \leftrightarrow \forall y\left(x=y\to \phi \right)$$
7	6	albii	$$⊢\forall x\left[x/y\right]\phi \leftrightarrow \forall x\forall y\left(x=y\to \phi \right)$$
8		sb6	$$⊢\left[y/x\right]\phi \leftrightarrow \forall x\left(x=y\to \phi \right)$$
9	8	albii	$$⊢\forall y\left[y/x\right]\phi \leftrightarrow \forall y\forall x\left(x=y\to \phi \right)$$
10	1 7 9	3bitr4i	$$⊢\forall x\left[x/y\right]\phi \leftrightarrow \forall y\left[y/x\right]\phi$$