Metamath Proof Explorer

Theorem sbbibOLD

Description: Obsolete version of sbbib as of 4-Sep-2023. (Contributed by AV, 6-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses sbbibOLD.y ⊢ Ⅎ 𝑦 𝜑
sbbibOLD.x ⊢ Ⅎ 𝑥 𝜓
Assertion sbbibOLD ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )

Proof

Step Hyp Ref Expression
1 sbbibOLD.y ⊢ Ⅎ 𝑦 𝜑
2 sbbibOLD.x ⊢ Ⅎ 𝑥 𝜓
3 nfs1v ⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
4 3 2 nfbi ⊢ Ⅎ 𝑥 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
5 4 nf5ri ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) → ∀ 𝑥 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
6 5 hbal ⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) → ∀ 𝑥 ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
7 sbcov ⊢ ( [ 𝑥 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜑 )
8 1 sbf ⊢ ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 )
9 7 8 bitri ⊢ ( [ 𝑥 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 )
10 spsbbi ⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) → ( [ 𝑥 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )
11 9 10 bitr3id ⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) → ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )
12 6 11 alrimih ⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) → ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )
13 nfs1v ⊢ Ⅎ 𝑦 [ 𝑥 / 𝑦 ] 𝜓
14 1 13 nfbi ⊢ Ⅎ 𝑦 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 )
15 14 nf5ri ⊢ ( ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) → ∀ 𝑦 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )
16 15 hbal ⊢ ( ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) → ∀ 𝑦 ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )
17 spsbbi ⊢ ( ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑥 / 𝑦 ] 𝜓 ) )
18 sbcov ⊢ ( [ 𝑦 / 𝑥 ] [ 𝑥 / 𝑦 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜓 )
19 2 sbf ⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝜓 )
20 18 19 bitri ⊢ ( [ 𝑦 / 𝑥 ] [ 𝑥 / 𝑦 ] 𝜓 ↔ 𝜓 )
21 17 20 bitrdi ⊢ ( ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
22 16 21 alrimih ⊢ ( ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) → ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
23 12 22 impbii ⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜓 ) )