Theorem sb8f

Description: Substitution of variable in universal quantifier. Version of sb8 with a disjoint variable condition, not requiring ax-10 or ax-13 . (Contributed by NM, 16-May-1993) (Revised by Wolf Lammen, 19-Jan-2023) Avoid ax-10 . (Revised by SN, 5-Dec-2024)

	Ref	Expression
Hypothesis	sb8f.nf	$$⊢Ⅎy\phi$$
Assertion	sb8f	$$⊢\forall x\phi \leftrightarrow \forall y\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		sb8f.nf	$$⊢Ⅎy\phi$$
2		sb6	$$⊢\left[y/x\right]\phi \leftrightarrow \forall x\left(x=y\to \phi \right)$$
3	2	albii	$$⊢\forall y\left[y/x\right]\phi \leftrightarrow \forall y\forall x\left(x=y\to \phi \right)$$
4		alcom	$$⊢\forall y\forall x\left(x=y\to \phi \right)\leftrightarrow \forall x\forall y\left(x=y\to \phi \right)$$
5		sb6	$$⊢\left[x/y\right]\phi \leftrightarrow \forall y\left(y=x\to \phi \right)$$
6	1	sbf	$$⊢\left[x/y\right]\phi \leftrightarrow \phi$$
7		equcom	$$⊢y=x\leftrightarrow x=y$$
8	7	imbi1i	$$⊢\left(y=x\to \phi \right)\leftrightarrow \left(x=y\to \phi \right)$$
9	8	albii	$$⊢\forall y\left(y=x\to \phi \right)\leftrightarrow \forall y\left(x=y\to \phi \right)$$
10	5 6 9	3bitr3ri	$$⊢\forall y\left(x=y\to \phi \right)\leftrightarrow \phi$$
11	10	albii	$$⊢\forall x\forall y\left(x=y\to \phi \right)\leftrightarrow \forall x\phi$$
12	3 4 11	3bitrri	$$⊢\forall x\phi \leftrightarrow \forall y\left[y/x\right]\phi$$