Theorem sbnf2

Description: Two ways of expressing " x is (effectively) not free in ph ". (Contributed by Gérard Lang, 14-Nov-2013) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 22-Sep-2018) Avoid ax-13 . (Revised by Wolf Lammen, 30-Jan-2023)

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

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ y ph
2	1	sb8ef	|- ( E. x ph <-> E. y [ y / x ] ph )
3		sb8v	|- ( A. x ph <-> A. z [ z / x ] ph )
4	2 3	imbi12i	|- ( ( E. x ph -> A. x ph ) <-> ( E. y [ y / x ] ph -> A. z [ z / x ] ph ) )
5		df-nf	|- ( F/ x ph <-> ( E. x ph -> A. x ph ) )
6		pm11.53v	|- ( A. y A. z ( [ y / x ] ph -> [ z / x ] ph ) <-> ( E. y [ y / x ] ph -> A. z [ z / x ] ph ) )
7	4 5 6	3bitr4i	|- ( F/ x ph <-> A. y A. z ( [ y / x ] ph -> [ z / x ] ph ) )
8		nfv	|- F/ z ph
9	8	sb8ef	|- ( E. x ph <-> E. z [ z / x ] ph )
10		sb8v	|- ( A. x ph <-> A. y [ y / x ] ph )
11	9 10	imbi12i	|- ( ( E. x ph -> A. x ph ) <-> ( E. z [ z / x ] ph -> A. y [ y / x ] ph ) )
12		pm11.53v	|- ( A. z A. y ( [ z / x ] ph -> [ y / x ] ph ) <-> ( E. z [ z / x ] ph -> A. y [ y / x ] ph ) )
13	11 5 12	3bitr4i	|- ( F/ x ph <-> A. z A. y ( [ z / x ] ph -> [ y / x ] ph ) )
14		alcom	|- ( A. z A. y ( [ z / x ] ph -> [ y / x ] ph ) <-> A. y A. z ( [ z / x ] ph -> [ y / x ] ph ) )
15	13 14	bitri	|- ( F/ x ph <-> A. y A. z ( [ z / x ] ph -> [ y / x ] ph ) )
16	7 15	anbi12i	|- ( ( F/ x ph /\ F/ x ph ) <-> ( A. y A. z ( [ y / x ] ph -> [ z / x ] ph ) /\ A. y A. z ( [ z / x ] ph -> [ y / x ] ph ) ) )
17		pm4.24	|- ( F/ x ph <-> ( F/ x ph /\ F/ x ph ) )
18		2albiim	|- ( A. y A. z ( [ y / x ] ph <-> [ z / x ] ph ) <-> ( A. y A. z ( [ y / x ] ph -> [ z / x ] ph ) /\ A. y A. z ( [ z / x ] ph -> [ y / x ] ph ) ) )
19	16 17 18	3bitr4i	|- ( F/ x ph <-> A. y A. z ( [ y / x ] ph <-> [ z / x ] ph ) )