Theorem sbnf2

Description: Two ways of expressing " x is (effectively) not free in ph ". (Contributed by Gérard Lang, 14-Nov-2013) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 22-Sep-2018) Avoid ax-13 . (Revised by Wolf Lammen, 30-Jan-2023)

	Ref	Expression
Assertion	sbnf2	⊢ ( Ⅎ 𝑥 𝜑 ↔ ∀ 𝑦 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑦 𝜑
2	1	sb8ef	⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
3		sb8v	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑧 [ 𝑧 / 𝑥 ] 𝜑 )
4	2 3	imbi12i	⊢ ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑧 / 𝑥 ] 𝜑 ) )
5		df-nf	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) )
6		pm11.53v	⊢ ( ∀ 𝑦 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑧 / 𝑥 ] 𝜑 ) )
7	4 5 6	3bitr4i	⊢ ( Ⅎ 𝑥 𝜑 ↔ ∀ 𝑦 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) )
8		nfv	⊢ Ⅎ 𝑧 𝜑
9	8	sb8ef	⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑧 [ 𝑧 / 𝑥 ] 𝜑 )
10		sb8v	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
11	9 10	imbi12i	⊢ ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( ∃ 𝑧 [ 𝑧 / 𝑥 ] 𝜑 → ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
12		pm11.53v	⊢ ( ∀ 𝑧 ∀ 𝑦 ( [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( ∃ 𝑧 [ 𝑧 / 𝑥 ] 𝜑 → ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
13	11 5 12	3bitr4i	⊢ ( Ⅎ 𝑥 𝜑 ↔ ∀ 𝑧 ∀ 𝑦 ( [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
14		alcom	⊢ ( ∀ 𝑧 ∀ 𝑦 ( [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑧 ( [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
15	13 14	bitri	⊢ ( Ⅎ 𝑥 𝜑 ↔ ∀ 𝑦 ∀ 𝑧 ( [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
16	7 15	anbi12i	⊢ ( ( Ⅎ 𝑥 𝜑 ∧ Ⅎ 𝑥 𝜑 ) ↔ ( ∀ 𝑦 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑦 ∀ 𝑧 ( [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
17		pm4.24	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( Ⅎ 𝑥 𝜑 ∧ Ⅎ 𝑥 𝜑 ) )
18		2albiim	⊢ ( ∀ 𝑦 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( ∀ 𝑦 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ∀ 𝑦 ∀ 𝑧 ( [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
19	16 17 18	3bitr4i	⊢ ( Ⅎ 𝑥 𝜑 ↔ ∀ 𝑦 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )