Theorem sbnfOLD

Description: Obsolete version of sbnf as of 2-May-2025. (Contributed by BJ, 2-May-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sbnfOLD	|- ( [ z / y ] F/ x ph <-> F/ x [ z / y ] ph )

Proof

Step	Hyp	Ref	Expression
1		sbim	|- ( [ z / y ] ( ph -> A. x ph ) <-> ( [ z / y ] ph -> [ z / y ] A. x ph ) )
2		sbal	|- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
3	2	imbi2i	|- ( ( [ z / y ] ph -> [ z / y ] A. x ph ) <-> ( [ z / y ] ph -> A. x [ z / y ] ph ) )
4	1 3	bitri	|- ( [ z / y ] ( ph -> A. x ph ) <-> ( [ z / y ] ph -> A. x [ z / y ] ph ) )
5	4	albii	|- ( A. x [ z / y ] ( ph -> A. x ph ) <-> A. x ( [ z / y ] ph -> A. x [ z / y ] ph ) )
6		nf5	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
7	6	sbbii	|- ( [ z / y ] F/ x ph <-> [ z / y ] A. x ( ph -> A. x ph ) )
8		sbal	|- ( [ z / y ] A. x ( ph -> A. x ph ) <-> A. x [ z / y ] ( ph -> A. x ph ) )
9	7 8	bitri	|- ( [ z / y ] F/ x ph <-> A. x [ z / y ] ( ph -> A. x ph ) )
10		nf5	|- ( F/ x [ z / y ] ph <-> A. x ( [ z / y ] ph -> A. x [ z / y ] ph ) )
11	5 9 10	3bitr4i	|- ( [ z / y ] F/ x ph <-> F/ x [ z / y ] ph )