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	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall y\forall z⦋y/x⦌A=⦋z/x⦌A$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2		csbtt	$$⊢\left(y\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xA\right)\to ⦋y/x⦌A=A$$
3	1 2	mpan	$$⊢\underset{\_}{Ⅎ}xA\to ⦋y/x⦌A=A$$
4		vex	$$⊢z\in \mathrm{V}$$
5		csbtt	$$⊢\left(z\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xA\right)\to ⦋z/x⦌A=A$$
6	4 5	mpan	$$⊢\underset{\_}{Ⅎ}xA\to ⦋z/x⦌A=A$$
7	3 6	eqtr4d	$$⊢\underset{\_}{Ⅎ}xA\to ⦋y/x⦌A=⦋z/x⦌A$$
8	7	alrimivv	$$⊢\underset{\_}{Ⅎ}xA\to \forall y\forall z⦋y/x⦌A=⦋z/x⦌A$$
9		nfv	$$⊢Ⅎw\forall y\forall z⦋y/x⦌A=⦋z/x⦌A$$
10		eleq2	$$⊢⦋y/x⦌A=⦋z/x⦌A\to \left(w\in ⦋y/x⦌A\leftrightarrow w\in ⦋z/x⦌A\right)$$
11		sbsbc	$$⊢\left[y/x\right]w\in A\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}w\in A$$
12		sbcel2	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}w\in A\leftrightarrow w\in ⦋y/x⦌A$$
13	11 12	bitri	$$⊢\left[y/x\right]w\in A\leftrightarrow w\in ⦋y/x⦌A$$
14		sbsbc	$$⊢\left[z/x\right]w\in A\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}w\in A$$
15		sbcel2	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}w\in A\leftrightarrow w\in ⦋z/x⦌A$$
16	14 15	bitri	$$⊢\left[z/x\right]w\in A\leftrightarrow w\in ⦋z/x⦌A$$
17	10 13 16	3bitr4g	$$⊢⦋y/x⦌A=⦋z/x⦌A\to \left(\left[y/x\right]w\in A\leftrightarrow \left[z/x\right]w\in A\right)$$
18	17	2alimi	$$⊢\forall y\forall z⦋y/x⦌A=⦋z/x⦌A\to \forall y\forall z\left(\left[y/x\right]w\in A\leftrightarrow \left[z/x\right]w\in A\right)$$
19		sbnf2	$$⊢Ⅎxw\in A\leftrightarrow \forall y\forall z\left(\left[y/x\right]w\in A\leftrightarrow \left[z/x\right]w\in A\right)$$
20	18 19	sylibr	$$⊢\forall y\forall z⦋y/x⦌A=⦋z/x⦌A\to Ⅎxw\in A$$
21	9 20	nfcd	$$⊢\forall y\forall z⦋y/x⦌A=⦋z/x⦌A\to \underset{\_}{Ⅎ}xA$$
22	8 21	impbii	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall y\forall z⦋y/x⦌A=⦋z/x⦌A$$