This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfich2

Description: Alternate definition of the property of a wff ph that the setvar variables x and y are interchangeable. (Contributed by AV and WL, 6-Aug-2023)

Ref Expression
Assertion dfich2 ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-ich ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
2 nfs1v ⊢ Ⅎ 𝑦 [ 𝑏 / 𝑦 ] 𝜑
3 2 nfsbv ⊢ Ⅎ 𝑦 [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑
4 3 nfsbv ⊢ Ⅎ 𝑦 [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑
5 nfv ⊢ Ⅎ 𝑎 𝜑
6 4 5 sbbib ⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ 𝜑 ) ↔ ∀ 𝑎 ( [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) )
7 6 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑎 ( [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) )
8 sbco4 ⊢ ( [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
9 8 bibi1i ⊢ ( ( [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ 𝜑 ) ↔ ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
10 9 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( [ 𝑦 / 𝑎 ] [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
11 alcom ⊢ ( ∀ 𝑥 ∀ 𝑎 ( [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) ↔ ∀ 𝑎 ∀ 𝑥 ( [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) )
12 nfs1v ⊢ Ⅎ 𝑥 [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑
13 nfv ⊢ Ⅎ 𝑏 [ 𝑎 / 𝑦 ] 𝜑
14 12 13 sbbib ⊢ ( ∀ 𝑥 ( [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) ↔ ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) )
15 14 albii ⊢ ( ∀ 𝑎 ∀ 𝑥 ( [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) )
16 11 15 bitri ⊢ ( ∀ 𝑥 ∀ 𝑎 ( [ 𝑥 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) )
17 7 10 16 3bitr3i ⊢ ( ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 ) ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) )
18 1 17 bitri ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) )