Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbbibOLD Structured version   Visualization version   GIF version

Theorem sbbibOLD 2289
 Description: Obsolete version of sbbib 2380 as of 4-Sep-2023. (Contributed by AV, 6-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
sbbibOLD.y 𝑦𝜑
sbbibOLD.x 𝑥𝜓
Assertion
Ref Expression
sbbibOLD (∀𝑦([𝑦 / 𝑥]𝜑𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem sbbibOLD
StepHypRef Expression
1 nfs1v 2160 . . . . . 6 𝑥[𝑦 / 𝑥]𝜑
2 sbbibOLD.x . . . . . 6 𝑥𝜓
31, 2nfbi 1904 . . . . 5 𝑥([𝑦 / 𝑥]𝜑𝜓)
43nf5ri 2195 . . . 4 (([𝑦 / 𝑥]𝜑𝜓) → ∀𝑥([𝑦 / 𝑥]𝜑𝜓))
54hbal 2174 . . 3 (∀𝑦([𝑦 / 𝑥]𝜑𝜓) → ∀𝑥𝑦([𝑦 / 𝑥]𝜑𝜓))
6 sbcov 2258 . . . . 5 ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)
7 sbbibOLD.y . . . . . 6 𝑦𝜑
87sbf 2271 . . . . 5 ([𝑥 / 𝑦]𝜑𝜑)
96, 8bitri 277 . . . 4 ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑𝜑)
10 spsbbi 2078 . . . 4 (∀𝑦([𝑦 / 𝑥]𝜑𝜓) → ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜓))
119, 10syl5bbr 287 . . 3 (∀𝑦([𝑦 / 𝑥]𝜑𝜓) → (𝜑 ↔ [𝑥 / 𝑦]𝜓))
125, 11alrimih 1824 . 2 (∀𝑦([𝑦 / 𝑥]𝜑𝜓) → ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
13 nfs1v 2160 . . . . . 6 𝑦[𝑥 / 𝑦]𝜓
147, 13nfbi 1904 . . . . 5 𝑦(𝜑 ↔ [𝑥 / 𝑦]𝜓)
1514nf5ri 2195 . . . 4 ((𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦(𝜑 ↔ [𝑥 / 𝑦]𝜓))
1615hbal 2174 . . 3 (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
17 spsbbi 2078 . . . 4 (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑥 / 𝑦]𝜓))
18 sbcov 2258 . . . . 5 ([𝑦 / 𝑥][𝑥 / 𝑦]𝜓 ↔ [𝑦 / 𝑥]𝜓)
192sbf 2271 . . . . 5 ([𝑦 / 𝑥]𝜓𝜓)
2018, 19bitri 277 . . . 4 ([𝑦 / 𝑥][𝑥 / 𝑦]𝜓𝜓)
2117, 20syl6bb 289 . . 3 (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ([𝑦 / 𝑥]𝜑𝜓))
2216, 21alrimih 1824 . 2 (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦([𝑦 / 𝑥]𝜑𝜓))
2312, 22impbii 211 1 (∀𝑦([𝑦 / 𝑥]𝜑𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208  ∀wal 1535  Ⅎwnf 1784  [wsb 2069 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145  ax-11 2161  ax-12 2177 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator