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

Metamath Proof Explorer

Theorem icheq

Description: In an equality of setvar variables, the setvar variables are interchangeable. (Contributed by AV, 29-Jul-2023)

Ref Expression
Assertion icheq 
|- [ x <> y ] x = y

Proof

Step Hyp Ref Expression
1 equsb3r 
 |-  ( [ z / y ] x = y <-> x = z )
2 1 2sbbii 
 |-  ( [ x / z ] [ y / x ] [ z / y ] x = y <-> [ x / z ] [ y / x ] x = z )
3 equsb3 
 |-  ( [ y / x ] x = z <-> y = z )
4 3 sbbii 
 |-  ( [ x / z ] [ y / x ] x = z <-> [ x / z ] y = z )
5 equsb3r 
 |-  ( [ x / z ] y = z <-> y = x )
6 equcom 
 |-  ( y = x <-> x = y )
7 5 6 bitri 
 |-  ( [ x / z ] y = z <-> x = y )
8 2 4 7 3bitri 
 |-  ( [ x / z ] [ y / x ] [ z / y ] x = y <-> x = y )
9 8 gen2 
 |-  A. x A. y ( [ x / z ] [ y / x ] [ z / y ] x = y <-> x = y )
10 df-ich 
 |-  ( [ x <> y ] x = y <-> A. x A. y ( [ x / z ] [ y / x ] [ z / y ] x = y <-> x = y ) )
11 9 10 mpbir 
 |-  [ x <> y ] x = y