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	|- ( ( ph -> A. x ph ) <-> A. y ( ph -> [ y / x ] ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ y ph
2	1	sb8	|- ( A. x ph <-> A. y [ y / x ] ph )
3	2	imbi2i	|- ( ( ph -> A. x ph ) <-> ( ph -> A. y [ y / x ] ph ) )
4		19.21v	|- ( A. y ( ph -> [ y / x ] ph ) <-> ( ph -> A. y [ y / x ] ph ) )
5	3 4	bitr4i	|- ( ( ph -> A. x ph ) <-> A. y ( ph -> [ y / x ] ph ) )