Theorem ichcom

Description: The interchangeability of setvar variables is commutative. (Contributed by AV, 20-Aug-2023)

	Ref	Expression
Assertion	ichcom	|- ( [ x <> y ] ps <-> [ y <> x ] ps )

Proof

Step	Hyp	Ref	Expression
1		alcom	|- ( A. b A. a ( [ b / x ] [ a / y ] ps <-> [ a / x ] [ b / y ] ps ) <-> A. a A. b ( [ b / x ] [ a / y ] ps <-> [ a / x ] [ b / y ] ps ) )
2		sbcom2	|- ( [ b / x ] [ a / y ] ps <-> [ a / y ] [ b / x ] ps )
3		sbcom2	|- ( [ a / x ] [ b / y ] ps <-> [ b / y ] [ a / x ] ps )
4	2 3	bibi12i	|- ( ( [ b / x ] [ a / y ] ps <-> [ a / x ] [ b / y ] ps ) <-> ( [ a / y ] [ b / x ] ps <-> [ b / y ] [ a / x ] ps ) )
5	4	2albii	|- ( A. a A. b ( [ b / x ] [ a / y ] ps <-> [ a / x ] [ b / y ] ps ) <-> A. a A. b ( [ a / y ] [ b / x ] ps <-> [ b / y ] [ a / x ] ps ) )
6	1 5	bitri	|- ( A. b A. a ( [ b / x ] [ a / y ] ps <-> [ a / x ] [ b / y ] ps ) <-> A. a A. b ( [ a / y ] [ b / x ] ps <-> [ b / y ] [ a / x ] ps ) )
7		dfich2	|- ( [ x <> y ] ps <-> A. b A. a ( [ b / x ] [ a / y ] ps <-> [ a / x ] [ b / y ] ps ) )
8		dfich2	|- ( [ y <> x ] ps <-> A. a A. b ( [ a / y ] [ b / x ] ps <-> [ b / y ] [ a / x ] ps ) )
9	6 7 8	3bitr4i	|- ( [ x <> y ] ps <-> [ y <> x ] ps )