Theorem ichn

Description: Negation does not affect interchangeability. (Contributed by SN, 30-Aug-2023)

	Ref	Expression
Assertion	ichn	⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ [ 𝑎 ⇄ 𝑏 ] ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		notbi	⊢ ( ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) ↔ ( ¬ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ ¬ 𝜑 ) )
2		sbn	⊢ ( [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ [ 𝑢 / 𝑏 ] 𝜑 )
3	2	sbbii	⊢ ( [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ [ 𝑏 / 𝑎 ] ¬ [ 𝑢 / 𝑏 ] 𝜑 )
4		sbn	⊢ ( [ 𝑏 / 𝑎 ] ¬ [ 𝑢 / 𝑏 ] 𝜑 ↔ ¬ [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
5	3 4	bitri	⊢ ( [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
6	5	sbbii	⊢ ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ [ 𝑎 / 𝑢 ] ¬ [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
7		sbn	⊢ ( [ 𝑎 / 𝑢 ] ¬ [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ ¬ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
8	6 7	bitri	⊢ ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 )
9	8	bibi1i	⊢ ( ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ 𝜑 ) ↔ ( ¬ [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ ¬ 𝜑 ) )
10	1 9	bitr4i	⊢ ( ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) ↔ ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ 𝜑 ) )
11	10	2albii	⊢ ( ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ 𝜑 ) )
12		df-ich	⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
13		df-ich	⊢ ( [ 𝑎 ⇄ 𝑏 ] ¬ 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑢 ] [ 𝑏 / 𝑎 ] [ 𝑢 / 𝑏 ] ¬ 𝜑 ↔ ¬ 𝜑 ) )
14	11 12 13	3bitr4i	⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ [ 𝑎 ⇄ 𝑏 ] ¬ 𝜑 )