Theorem ichnfb

Description: If x and y are interchangeable in ph , they are both free or both not free in ph . (Contributed by Wolf Lammen, 6-Aug-2023) (Revised by AV, 23-Sep-2023)

	Ref	Expression
Assertion	ichnfb	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 → ( ∀ 𝑥 Ⅎ 𝑦 𝜑 ↔ ∀ 𝑦 Ⅎ 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		ichcom	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ [ 𝑦 ⇄ 𝑥 ] 𝜑 )
2		ichnfim	⊢ ( ( ∀ 𝑥 Ⅎ 𝑦 𝜑 ∧ [ 𝑦 ⇄ 𝑥 ] 𝜑 ) → ∀ 𝑦 Ⅎ 𝑥 𝜑 )
3	1 2	sylan2b	⊢ ( ( ∀ 𝑥 Ⅎ 𝑦 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 ) → ∀ 𝑦 Ⅎ 𝑥 𝜑 )
4	3	expcom	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 → ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ∀ 𝑦 Ⅎ 𝑥 𝜑 ) )
5		ichnfim	⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 ) → ∀ 𝑥 Ⅎ 𝑦 𝜑 )
6	5	expcom	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 → ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ∀ 𝑥 Ⅎ 𝑦 𝜑 ) )
7	4 6	impbid	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 → ( ∀ 𝑥 Ⅎ 𝑦 𝜑 ↔ ∀ 𝑦 Ⅎ 𝑥 𝜑 ) )