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

Theorem dfich2 43972
Description: Alternate definition of the propery of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. (Contributed by AV and WL, 6-Aug-2023.)
Assertion
Ref Expression
dfich2 ([𝑥𝑦]𝜑 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
Distinct variable groups:   𝑎,𝑏,𝜑   𝑥,𝑎,𝑦,𝑏
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem dfich2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-ich 43960 . 2 ([𝑥𝑦]𝜑 ↔ ∀𝑥𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑𝜑))
2 nfs1v 2158 . . . . . . 7 𝑦[𝑏 / 𝑦]𝜑
32nfsbv 2341 . . . . . 6 𝑦[𝑎 / 𝑥][𝑏 / 𝑦]𝜑
43nfsbv 2341 . . . . 5 𝑦[𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑
5 nfv 1915 . . . . 5 𝑎𝜑
64, 5sbbib 2372 . . . 4 (∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜑) ↔ ∀𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑))
76albii 1821 . . 3 (∀𝑥𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜑) ↔ ∀𝑥𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑))
8 sbco4 2282 . . . . 5 ([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑)
98bibi1i 342 . . . 4 (([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜑) ↔ ([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑𝜑))
1092albii 1822 . . 3 (∀𝑥𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜑) ↔ ∀𝑥𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑𝜑))
11 alcom 2161 . . . 4 (∀𝑥𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑎𝑥([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑))
12 nfs1v 2158 . . . . . 6 𝑥[𝑎 / 𝑥][𝑏 / 𝑦]𝜑
13 nfv 1915 . . . . . 6 𝑏[𝑎 / 𝑦]𝜑
1412, 13sbbib 2372 . . . . 5 (∀𝑥([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
1514albii 1821 . . . 4 (∀𝑎𝑥([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
1611, 15bitri 278 . . 3 (∀𝑥𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
177, 10, 163bitr3i 304 . 2 (∀𝑥𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑𝜑) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
181, 17bitri 278 1 ([𝑥𝑦]𝜑 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wal 1536  [wsb 2069  [wich 43959
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 2143  ax-11 2159  ax-12 2176
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 43960
This theorem is referenced by:  ichcom  43973  ichbi12i  43974  ichnfim  43978  ichnreuop  43986  ichreuopeq  43987
  Copyright terms: Public domain W3C validator