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

Definition df-ich 46780
Description: Define the property of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. For an alternate definition using implicit substitution and a temporary setvar variable see ichcircshi 46788. Another, equivalent definition using two temporary setvar variables is provided in dfich2 46792. (Contributed by AV, 29-Jul-2023.)
Assertion
Ref Expression
df-ich ([𝑥𝑦]𝜑 ↔ ∀𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑𝜑))
Distinct variable groups:   𝜑,𝑎   𝑥,𝑎   𝑦,𝑎
Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Definition df-ich
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
41, 2, 3wich 46779 . 2 wff [𝑥𝑦]𝜑
5 va . . . . . . . 8 setvar 𝑎
61, 3, 5wsb 2060 . . . . . . 7 wff [𝑎 / 𝑦]𝜑
76, 2, 3wsb 2060 . . . . . 6 wff [𝑦 / 𝑥][𝑎 / 𝑦]𝜑
87, 5, 2wsb 2060 . . . . 5 wff [𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑
98, 1wb 205 . . . 4 wff ([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑𝜑)
109, 3wal 1532 . . 3 wff 𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑𝜑)
1110, 2wal 1532 . 2 wff 𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑𝜑)
124, 11wb 205 1 wff ([𝑥𝑦]𝜑 ↔ ∀𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  nfich1  46781  nfich2  46782  ichv  46783  ichf  46784  ichid  46785  icht  46786  ichbidv  46787  ichcircshi  46788  ichan  46789  ichn  46790  dfich2  46792  icheq  46796  ichal  46800  ich2exprop  46805
  Copyright terms: Public domain W3C validator