Metamath Proof Explorer


Theorem ichid

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

Ref Expression
Assertion ichid x x φ

Proof

Step Hyp Ref Expression
1 sbid x x a x φ a x φ
2 1 sbbii x a x x a x φ x a a x φ
3 sbid2vw x a a x φ φ
4 2 3 bitri x a x x a x φ φ
5 4 gen2 x x x a x x a x φ φ
6 df-ich x x φ x x x a x x a x φ φ
7 5 6 mpbir x x φ