Metamath Proof Explorer


Theorem ichid

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

Ref Expression
Assertion ichid [ 𝑥𝑥 ] 𝜑

Proof

Step Hyp Ref Expression
1 sbid ( [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] 𝜑 )
2 1 sbbii ( [ 𝑥 / 𝑎 ] [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] [ 𝑎 / 𝑥 ] 𝜑 )
3 sbid2vw ( [ 𝑥 / 𝑎 ] [ 𝑎 / 𝑥 ] 𝜑𝜑 )
4 2 3 bitri ( [ 𝑥 / 𝑎 ] [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑𝜑 )
5 4 gen2 𝑥𝑥 ( [ 𝑥 / 𝑎 ] [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑𝜑 )
6 df-ich ( [ 𝑥𝑥 ] 𝜑 ↔ ∀ 𝑥𝑥 ( [ 𝑥 / 𝑎 ] [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑𝜑 ) )
7 5 6 mpbir [ 𝑥𝑥 ] 𝜑