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	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) )