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 45620
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 45608 . 2 ([𝑥𝑦]𝜑 ↔ ∀𝑥𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑𝜑))
2 nfs1v 2153 . . . . . . 7 𝑦[𝑏 / 𝑦]𝜑
32nfsbv 2323 . . . . . 6 𝑦[𝑎 / 𝑥][𝑏 / 𝑦]𝜑
43nfsbv 2323 . . . . 5 𝑦[𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑
5 nfv 1917 . . . . 5 𝑎𝜑
64, 5sbbib 2357 . . . 4 (∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜑) ↔ ∀𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑))
76albii 1821 . . 3 (∀𝑥𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜑) ↔ ∀𝑥𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑))
8 sbco4 2274 . . . . 5 ([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑)
98bibi1i 338 . . . 4 (([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜑) ↔ ([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑𝜑))
1092albii 1822 . . 3 (∀𝑥𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜑) ↔ ∀𝑥𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑𝜑))
11 alcom 2156 . . . 4 (∀𝑥𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑎𝑥([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑))
12 nfs1v 2153 . . . . . 6 𝑥[𝑎 / 𝑥][𝑏 / 𝑦]𝜑
13 nfv 1917 . . . . . 6 𝑏[𝑎 / 𝑦]𝜑
1412, 13sbbib 2357 . . . . 5 (∀𝑥([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
1514albii 1821 . . . 4 (∀𝑎𝑥([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
1611, 15bitri 274 . . 3 (∀𝑥𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
177, 10, 163bitr3i 300 . 2 (∀𝑥𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑𝜑) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
181, 17bitri 274 1 ([𝑥𝑦]𝜑 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wal 1539  [wsb 2067  [wich 45607
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 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-ich 45608
This theorem is referenced by:  ichcom  45621  ichbi12i  45622  ichnfim  45626  ichnreuop  45634  ichreuopeq  45635
  Copyright terms: Public domain W3C validator