Theorem wl-sb6rft

Description: A specialization of wl-equsal1t . Closed form of sb6rf . (Contributed by Wolf Lammen, 27-Jul-2019)

	Ref	Expression
Assertion	wl-sb6rft	$$⊢Ⅎx\phi \to \left(\phi \leftrightarrow \forall x\left(x=y\to \left[x/y\right]\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfnf1	$$⊢ℲxℲx\phi$$
2		id	$$⊢Ⅎx\phi \to Ⅎx\phi$$
3		sbequ12r	$$⊢x=y\to \left(\left[x/y\right]\phi \leftrightarrow \phi \right)$$
4	3	a1i	$$⊢Ⅎx\phi \to \left(x=y\to \left(\left[x/y\right]\phi \leftrightarrow \phi \right)\right)$$
5	1 2 4	wl-equsald	$$⊢Ⅎx\phi \to \left(\forall x\left(x=y\to \left[x/y\right]\phi \right)\leftrightarrow \phi \right)$$
6	5	bicomd	$$⊢Ⅎx\phi \to \left(\phi \leftrightarrow \forall x\left(x=y\to \left[x/y\right]\phi \right)\right)$$