Theorem sbhb

Description: Two ways of expressing " x is (effectively) not free in ph ". Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 29-May-2009) (New usage is discouraged.)

	Ref	Expression
Assertion	sbhb	$$⊢\left(\phi \to \forall x\phi \right)\leftrightarrow \forall y\left(\phi \to \left[y/x\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎy\phi$$
2	1	sb8	$$⊢\forall x\phi \leftrightarrow \forall y\left[y/x\right]\phi$$
3	2	imbi2i	$$⊢\left(\phi \to \forall x\phi \right)\leftrightarrow \left(\phi \to \forall y\left[y/x\right]\phi \right)$$
4		19.21v	$$⊢\forall y\left(\phi \to \left[y/x\right]\phi \right)\leftrightarrow \left(\phi \to \forall y\left[y/x\right]\phi \right)$$
5	3 4	bitr4i	$$⊢\left(\phi \to \forall x\phi \right)\leftrightarrow \forall y\left(\phi \to \left[y/x\right]\phi \right)$$