Theorem wl-sbhbt

Description: Closed form of sbhb . Characterizing the expression ph -> A. x ph using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		wl-sb8t	$$⊢\forall xℲy\phi \to \left(\forall x\phi \leftrightarrow \forall y\left[y/x\right]\phi \right)$$
2	1	imbi2d	$$⊢\forall xℲy\phi \to \left(\left(\phi \to \forall x\phi \right)\leftrightarrow \left(\phi \to \forall y\left[y/x\right]\phi \right)\right)$$
3		19.21t	$$⊢Ⅎy\phi \to \left(\forall y\left(\phi \to \left[y/x\right]\phi \right)\leftrightarrow \left(\phi \to \forall y\left[y/x\right]\phi \right)\right)$$
4	3	sps	$$⊢\forall xℲy\phi \to \left(\forall y\left(\phi \to \left[y/x\right]\phi \right)\leftrightarrow \left(\phi \to \forall y\left[y/x\right]\phi \right)\right)$$
5	2 4	bitr4d	$$⊢\forall xℲy\phi \to \left(\left(\phi \to \forall x\phi \right)\leftrightarrow \forall y\left(\phi \to \left[y/x\right]\phi \right)\right)$$