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	⊢ Ⅎ 𝑦 𝜑
	sbbib.x	⊢ Ⅎ 𝑥 𝜓
Assertion	sbbib	⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		sbbib.y	⊢ Ⅎ 𝑦 𝜑
2		sbbib.x	⊢ Ⅎ 𝑥 𝜓
3		nfs1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
4	3 2	nfbi	⊢ Ⅎ 𝑥 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
5		nfs1v	⊢ Ⅎ 𝑦 [ 𝑥 / 𝑦 ] 𝜓
6	1 5	nfbi	⊢ Ⅎ 𝑦 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 )
7		sbequ12r	⊢ ( 𝑦 = 𝑥 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) )
8		sbequ12	⊢ ( 𝑦 = 𝑥 → ( 𝜓 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )
9	7 8	bibi12d	⊢ ( 𝑦 = 𝑥 → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) ) )
10	4 6 9	cbvalv1	⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )