This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )