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 43960
 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 43968. Another, equivalent definition using two temporary setvar variables is provided in dfich2 43972. (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 43959 . 2 wff [𝑥𝑦]𝜑
5 va . . . . . . . 8 setvar 𝑎
61, 3, 5wsb 2069 . . . . . . 7 wff [𝑎 / 𝑦]𝜑
76, 2, 3wsb 2069 . . . . . 6 wff [𝑦 / 𝑥][𝑎 / 𝑦]𝜑
87, 5, 2wsb 2069 . . . . 5 wff [𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑
98, 1wb 209 . . . 4 wff ([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑𝜑)
109, 3wal 1536 . . 3 wff 𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑𝜑)
1110, 2wal 1536 . 2 wff 𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑𝜑)
124, 11wb 209 1 wff ([𝑥𝑦]𝜑 ↔ ∀𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑𝜑))
 Colors of variables: wff setvar class This definition is referenced by:  nfich1  43961  nfich2  43962  ichv  43963  ichf  43964  ichid  43965  icht  43966  ichbidv  43967  ichcircshi  43968  ichan  43969  ichn  43970  dfich2  43972  icheq  43976  ichal  43980  ich2exprop  43985
 Copyright terms: Public domain W3C validator