Theorem sbbib

Description: Reversal of substitution. (Contributed by AV, 6-Aug-2023) (Proof shortened by Wolf Lammen, 4-Sep-2023)

	Ref	Expression
Hypotheses	sbbib.y	$$⊢Ⅎy\phi$$
	sbbib.x	$$⊢Ⅎx\psi$$
Assertion	sbbib	$$⊢\forall y\left(\left[y/x\right]\phi \leftrightarrow \psi \right)\leftrightarrow \forall x\left(\phi \leftrightarrow \left[x/y\right]\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbbib.y	$$⊢Ⅎy\phi$$
2		sbbib.x	$$⊢Ⅎx\psi$$
3		nfs1v	$$⊢Ⅎx\left[y/x\right]\phi$$
4	3 2	nfbi	$$⊢Ⅎx\left(\left[y/x\right]\phi \leftrightarrow \psi \right)$$
5		nfs1v	$$⊢Ⅎy\left[x/y\right]\psi$$
6	1 5	nfbi	$$⊢Ⅎy\left(\phi \leftrightarrow \left[x/y\right]\psi \right)$$
7		sbequ12r	$$⊢y=x\to \left(\left[y/x\right]\phi \leftrightarrow \phi \right)$$
8		sbequ12	$$⊢y=x\to \left(\psi \leftrightarrow \left[x/y\right]\psi \right)$$
9	7 8	bibi12d	$$⊢y=x\to \left(\left(\left[y/x\right]\phi \leftrightarrow \psi \right)\leftrightarrow \left(\phi \leftrightarrow \left[x/y\right]\psi \right)\right)$$
10	4 6 9	cbvalv1	$$⊢\forall y\left(\left[y/x\right]\phi \leftrightarrow \psi \right)\leftrightarrow \forall x\left(\phi \leftrightarrow \left[x/y\right]\psi \right)$$