Metamath Proof Explorer


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 ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑𝜓 ) ↔ ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )