Metamath Proof Explorer


Definition df-ich

Description: Define the property of a wff ph that the setvar variables x and y are interchangeable. For an alternate definition using implicit substitution and a temporary setvar variable see ichcircshi . Another, equivalent definition using two temporary setvar variables is provided in dfich2 . (Contributed by AV, 29-Jul-2023)

Ref Expression
Assertion df-ich x y φ x y x a y x a y φ φ

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 vy setvar y
2 wph wff φ
3 2 0 1 wich wff x y φ
4 va setvar a
5 2 1 4 wsb wff a y φ
6 5 0 1 wsb wff y x a y φ
7 6 4 0 wsb wff x a y x a y φ
8 7 2 wb wff x a y x a y φ φ
9 8 1 wal wff y x a y x a y φ φ
10 9 0 wal wff x y x a y x a y φ φ
11 3 10 wb wff x y φ x y x a y x a y φ φ