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