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

Metamath Proof Explorer

Theorem ichf

Description: Setvar variables are interchangeable in a wff they are not free in. (Contributed by SN, 23-Nov-2023)

Ref Expression
Hypotheses ichf.1 
|- F/ x ph
ichf.2 
|- F/ y ph
Assertion ichf 
|- [ x <> y ] ph

Proof

Step Hyp Ref Expression
1 ichf.1 
 |-  F/ x ph
2 ichf.2 
 |-  F/ y ph
3 2 sbf 
 |-  ( [ a / y ] ph <-> ph )
4 3 sbbii 
 |-  ( [ y / x ] [ a / y ] ph <-> [ y / x ] ph )
5 1 sbf 
 |-  ( [ y / x ] ph <-> ph )
6 4 5 bitri 
 |-  ( [ y / x ] [ a / y ] ph <-> ph )
7 6 sbbii 
 |-  ( [ x / a ] [ y / x ] [ a / y ] ph <-> [ x / a ] ph )
8 sbv 
 |-  ( [ x / a ] ph <-> ph )
9 7 8 bitri 
 |-  ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph )
10 9 gen2 
 |-  A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph )
11 df-ich 
 |-  ( [ x <> y ] ph <-> A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) )
12 10 11 mpbir 
 |-  [ x <> y ] ph