Metamath Proof Explorer


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 [ 𝑥𝑦 ] 𝜑

Proof

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