Theorem ichv

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

	Ref	Expression
Assertion	ichv	|- [ x <> y ] ph

Proof

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