Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ichbi12i Structured version   Visualization version   GIF version

Theorem ichbi12i 43975
 Description: Equivalence for interchangeable setvar variables. (Contributed by AV, 29-Jul-2023.)
Hypothesis
Ref Expression
ichbi12i.1 ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜓𝜒))
Assertion
Ref Expression
ichbi12i ([𝑥𝑦]𝜓 ↔ [𝑎𝑏]𝜒)
Distinct variable groups:   𝑎,𝑏,𝜓   𝑥,𝑦,𝜒   𝑥,𝑎,𝑦,𝑏
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑎,𝑏)

Proof of Theorem ichbi12i
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1915 . . . . . . . . . 10 𝑏𝜓
21sbco2v 2341 . . . . . . . . 9 ([𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑦]𝜓)
32bicomi 227 . . . . . . . 8 ([𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
43sbbii 2081 . . . . . . 7 ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
5 sbcom2 2165 . . . . . . 7 ([𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
64, 5bitri 278 . . . . . 6 ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
76sbbii 2081 . . . . 5 ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
8 nfv 1915 . . . . . . 7 𝑎𝜓
98nfsbv 2338 . . . . . 6 𝑎[𝑣 / 𝑦]𝜓
109sbco2v 2341 . . . . 5 ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)
11 ichbi12i.1 . . . . . . 7 ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜓𝜒))
12112sbievw 2102 . . . . . 6 ([𝑎 / 𝑥][𝑏 / 𝑦]𝜓𝜒)
13122sbbii 2082 . . . . 5 ([𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
147, 10, 133bitr3i 304 . . . 4 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
15 sbcom2 2165 . . . . . . 7 ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓)
161sbco2v 2341 . . . . . . . 8 ([𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑦]𝜓)
1716sbbii 2081 . . . . . . 7 ([𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
1815, 17bitri 278 . . . . . 6 ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
1918sbbii 2081 . . . . 5 ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
20122sbbii 2082 . . . . 5 ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
218nfsbv 2338 . . . . . 6 𝑎[𝑢 / 𝑦]𝜓
2221sbco2v 2341 . . . . 5 ([𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓)
2319, 20, 223bitr3ri 305 . . . 4 ([𝑣 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
2414, 23bibi12i 343 . . 3 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
25242albii 1822 . 2 (∀𝑢𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ∀𝑢𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
26 dfich2 43973 . 2 ([𝑥𝑦]𝜓 ↔ ∀𝑢𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓))
27 dfich2 43973 . 2 ([𝑎𝑏]𝜒 ↔ ∀𝑢𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
2825, 26, 273bitr4i 306 1 ([𝑥𝑦]𝜓 ↔ [𝑎𝑏]𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  [wsb 2069  [wich 43960 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-11 2158  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-ich 43961 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator