Theorem bj-hbsb3v

Description: Version of hbsb3 with a disjoint variable condition, which does not require ax-13 . (Remark: the unbundled version of nfs1 is given by bj-nfs1v .) (Contributed by BJ, 11-Sep-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-hbsb3v.1	$$⊢\phi \to \forall y\phi$$
Assertion	bj-hbsb3v	$$⊢\left[y/x\right]\phi \to \forall x\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		bj-hbsb3v.1	$$⊢\phi \to \forall y\phi$$
2	1	sbimi	$$⊢\left[y/x\right]\phi \to \left[y/x\right]\forall y\phi$$
3		bj-hbsb2av	$$⊢\left[y/x\right]\forall y\phi \to \forall x\left[y/x\right]\phi$$
4	2 3	syl	$$⊢\left[y/x\right]\phi \to \forall x\left[y/x\right]\phi$$