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