Theorem ichid

Description: A setvar variable is always interchangeable with itself. (Contributed by AV, 29-Jul-2023)

	Ref	Expression
Assertion	ichid	|- [ x <> x ] ph

Proof

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