Metamath Proof Explorer


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 𝑥 𝜑
ichf.2 𝑦 𝜑
Assertion ichf [ 𝑥𝑦 ] 𝜑

Proof

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