Theorem sbnfc2

Description: Two ways of expressing " x is (effectively) not free in A ". (Contributed by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Assertion	sbnfc2	|- ( F/_ x A <-> A. y A. z [_ y / x ]_ A = [_ z / x ]_ A )

Proof

Step	Hyp	Ref	Expression
1		vex	|- y e. _V
2		csbtt	|- ( ( y e. _V /\ F/_ x A ) -> [_ y / x ]_ A = A )
3	1 2	mpan	|- ( F/_ x A -> [_ y / x ]_ A = A )
4		vex	|- z e. _V
5		csbtt	|- ( ( z e. _V /\ F/_ x A ) -> [_ z / x ]_ A = A )
6	4 5	mpan	|- ( F/_ x A -> [_ z / x ]_ A = A )
7	3 6	eqtr4d	|- ( F/_ x A -> [_ y / x ]_ A = [_ z / x ]_ A )
8	7	alrimivv	|- ( F/_ x A -> A. y A. z [_ y / x ]_ A = [_ z / x ]_ A )
9		nfv	|- F/ w A. y A. z [_ y / x ]_ A = [_ z / x ]_ A
10		eleq2	|- ( [_ y / x ]_ A = [_ z / x ]_ A -> ( w e. [_ y / x ]_ A <-> w e. [_ z / x ]_ A ) )
11		sbsbc	|- ( [ y / x ] w e. A <-> [. y / x ]. w e. A )
12		sbcel2	|- ( [. y / x ]. w e. A <-> w e. [_ y / x ]_ A )
13	11 12	bitri	|- ( [ y / x ] w e. A <-> w e. [_ y / x ]_ A )
14		sbsbc	|- ( [ z / x ] w e. A <-> [. z / x ]. w e. A )
15		sbcel2	|- ( [. z / x ]. w e. A <-> w e. [_ z / x ]_ A )
16	14 15	bitri	|- ( [ z / x ] w e. A <-> w e. [_ z / x ]_ A )
17	10 13 16	3bitr4g	|- ( [_ y / x ]_ A = [_ z / x ]_ A -> ( [ y / x ] w e. A <-> [ z / x ] w e. A ) )
18	17	2alimi	|- ( A. y A. z [_ y / x ]_ A = [_ z / x ]_ A -> A. y A. z ( [ y / x ] w e. A <-> [ z / x ] w e. A ) )
19		sbnf2	|- ( F/ x w e. A <-> A. y A. z ( [ y / x ] w e. A <-> [ z / x ] w e. A ) )
20	18 19	sylibr	|- ( A. y A. z [_ y / x ]_ A = [_ z / x ]_ A -> F/ x w e. A )
21	9 20	nfcd	|- ( A. y A. z [_ y / x ]_ A = [_ z / x ]_ A -> F/_ x A )
22	8 21	impbii	|- ( F/_ x A <-> A. y A. z [_ y / x ]_ A = [_ z / x ]_ A )