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	$$⊢Ⅎx\phi \leftrightarrow \forall y\forall z\left(\left[y/x\right]\phi \leftrightarrow \left[z/x\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎy\phi$$
2	1	sb8ef	$$⊢\exists x\phi \leftrightarrow \exists y\left[y/x\right]\phi$$
3		sb8v	$$⊢\forall x\phi \leftrightarrow \forall z\left[z/x\right]\phi$$
4	2 3	imbi12i	$$⊢\left(\exists x\phi \to \forall x\phi \right)\leftrightarrow \left(\exists y\left[y/x\right]\phi \to \forall z\left[z/x\right]\phi \right)$$
5		df-nf	$$⊢Ⅎx\phi \leftrightarrow \left(\exists x\phi \to \forall x\phi \right)$$
6		pm11.53v	$$⊢\forall y\forall z\left(\left[y/x\right]\phi \to \left[z/x\right]\phi \right)\leftrightarrow \left(\exists y\left[y/x\right]\phi \to \forall z\left[z/x\right]\phi \right)$$
7	4 5 6	3bitr4i	$$⊢Ⅎx\phi \leftrightarrow \forall y\forall z\left(\left[y/x\right]\phi \to \left[z/x\right]\phi \right)$$
8		nfv	$$⊢Ⅎz\phi$$
9	8	sb8ef	$$⊢\exists x\phi \leftrightarrow \exists z\left[z/x\right]\phi$$
10		sb8v	$$⊢\forall x\phi \leftrightarrow \forall y\left[y/x\right]\phi$$
11	9 10	imbi12i	$$⊢\left(\exists x\phi \to \forall x\phi \right)\leftrightarrow \left(\exists z\left[z/x\right]\phi \to \forall y\left[y/x\right]\phi \right)$$
12		pm11.53v	$$⊢\forall z\forall y\left(\left[z/x\right]\phi \to \left[y/x\right]\phi \right)\leftrightarrow \left(\exists z\left[z/x\right]\phi \to \forall y\left[y/x\right]\phi \right)$$
13	11 5 12	3bitr4i	$$⊢Ⅎx\phi \leftrightarrow \forall z\forall y\left(\left[z/x\right]\phi \to \left[y/x\right]\phi \right)$$
14		alcom	$$⊢\forall z\forall y\left(\left[z/x\right]\phi \to \left[y/x\right]\phi \right)\leftrightarrow \forall y\forall z\left(\left[z/x\right]\phi \to \left[y/x\right]\phi \right)$$
15	13 14	bitri	$$⊢Ⅎx\phi \leftrightarrow \forall y\forall z\left(\left[z/x\right]\phi \to \left[y/x\right]\phi \right)$$
16	7 15	anbi12i	$$⊢\left(Ⅎx\phi \wedge Ⅎx\phi \right)\leftrightarrow \left(\forall y\forall z\left(\left[y/x\right]\phi \to \left[z/x\right]\phi \right)\wedge \forall y\forall z\left(\left[z/x\right]\phi \to \left[y/x\right]\phi \right)\right)$$
17		pm4.24	$$⊢Ⅎx\phi \leftrightarrow \left(Ⅎx\phi \wedge Ⅎx\phi \right)$$
18		2albiim	$$⊢\forall y\forall z\left(\left[y/x\right]\phi \leftrightarrow \left[z/x\right]\phi \right)\leftrightarrow \left(\forall y\forall z\left(\left[y/x\right]\phi \to \left[z/x\right]\phi \right)\wedge \forall y\forall z\left(\left[z/x\right]\phi \to \left[y/x\right]\phi \right)\right)$$
19	16 17 18	3bitr4i	$$⊢Ⅎx\phi \leftrightarrow \forall y\forall z\left(\left[y/x\right]\phi \leftrightarrow \left[z/x\right]\phi \right)$$